Journal of Symbolic Logic 49 (3):730-753 (1984)
|Abstract||We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation|
|Keywords||No keywords specified (fix it)|
|Through your library||Configure|
Similar books and articles
Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65 (2):525-549.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Ingrid Lindström (1989). A Construction of Non-Well-Founded Sets Within Martin-Löf's Type Theory. Journal of Symbolic Logic 54 (1):57-64.
Giovanni Sambin & Jan M. Smith (eds.) (1998). Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995. Oxford University Press.
Erik Palmgren (1991). A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe. Journal of Symbolic Logic 56 (3):1012-1015.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Adam Obtułowicz (1989). Categorical and Algebraic Aspects of Martin-Löf Type Theory. Studia Logica 48 (3):299 - 317.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads2 ( #232,211 of 548,973 )
Recent downloads (6 months)0
How can I increase my downloads?