Type-Theoretical Approaches to Problems and Solutions

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F15%3A00083750" target="_blank" >RIV/00216224:14210/15:00083750 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Type-Theoretical Approaches to Problems and Solutions
Original language description
We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insightthat (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of
Czech name
—
Czech description
—

Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)