| 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: Set theory
2 matches
| Title | Type theory and proof processing system |
| Author | DOWEK Gilles |
| Keywords | Computation, Deduction, Function, Mathematical language, Proof, Proof processing systems, Set theory, Type theory |
| Topics | Computer Sciences, Computing, Logic, Sets, Software |
| Abstract | Since the end of the sixties, several computer programs allowing to process mathematical knowledge, and in particular mathematical proofs, have been designed. Building such programs raises new questions, in particular that of the conception of logical frameworks where mathematics can be formalized in practice. This is a new direction for fundational studies, more interested, so far, in formalization of mathematics in principle, than in practice. Several reasons explain that the designers of such programs often chose type theory rather than set theory to formalize mathematics. |
| Number | 165, Spring 2004, special issue: Constructive type theory |
| Language | French |
| 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