| 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:
- Parution: n° 165, Spring 2004, special issue: Constructive type theory
4 matches
| Title | Foreword. Special issue: "Type theory" |
| Author | BOURDEAU Michel, BOLDINI Pascal |
| Keywords | Type theory |
| Topics | Epistemology, History of Mathematics, Logic, Type Theory |
| Abstract | Foreword |
| Number | 165, Spring 2004, special issue: Constructive type theory |
| Language | French |
| 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 | Computational semantics in type theory |
| Author | RANTA Aarne |
| Keywords | Logical semantics, Montague grammar, Type theory |
| Topics | Computing, Linguistics, Logic, Semantics, Trees, Type Theory |
| Abstract | This paper aims to show how Montague-style grammars can be completely formalized and thereby declaratively implemented by using the Grammatical Framework GF. The implementation covers the fundamental operations of Montague's PTQ model: the construction of analysis trees, the linearization of trees into strings, and the interpretation of trees as logical formulas. Moreover, a parsing algorithm is derived from the grammar. Given that GF is a constructive type theory with dependent types, the technique extends from explain anaphoric reference. On the other hand, GF has a built-in compositionality requirement that is stronger than in PTQ and prevents us from formulating quantifying-in rules of Montague style. This leads us to alternative formulations of such rules in terms of combinators and discontinuous constituents. The PTQ fragment will moreover be presented as an example of how a GF grammar is modified by replacing English with another target language, French. The paper concludes by a discussion of the complementary rôles of logically and linguistically oriented syntax. |
| Number | 165, Spring 2004, special issue: Constructive type theory |
| Language |  English |
| 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