| Home |
| Last parution |
| Authors |
| Topics |
| Keywords |
| Parutions |
| Videos |
| Search |
| Reading committee |
| Contact |
| Subscription |
| Article submission |
French version |
The issues from 1 to 148 are also available on line at NUMDAM and at Revues.org for the following issues |
- Results for criterions:
- Keyword: Well-founded trees
1 match
| Title | Proof Theory of Martin-Löf Type Theory. An overview |
| Author | SETZER Anton |
| Keywords | Generic programming, Inductive-recursive definitions, Kleene's O, Kripke Platek set theory, Mahlo universe, Martin-Löf type theory, Set theory, Well-founded trees |
| Topics | Logic, Orders and preorders, Sets, Trees, Type Theory |
| Abstract | We give an overview over the historic development of proof theory and the main techniques used in ordinal theoretic proof theory. We argue, that in a revised Hilbert's program, ordinal theoretic proof theory has to be supplemented by a second step, namely the development of strong equiconsistent constructive theories. Then we show, how, as part of such a programe, the proof theoretic analysis of Martin-Löf type theory with W-type and one microscopic universe containing only two finite sets is carried out. Then we look at the analysis Martin-Löf type theory with W-type and a universe closed under the W-type, and consider the extension of type theory by one Mahlo universe and its proof-theoretic analysis. Finally, we repeat the concept of inductive-recursive definitions, which extends the notion of inductive definitions substantially. We introduce a closed formalization, which can be used in generic programming, and explain, what is known about its strength. |
| Number | 165, Spring 2004, special issue: Constructive type theory |
| Language |  English |
The entire journal is licensed under a Creative Commons license