of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has dependent types x : A B(x), which are regarded as indexed families of types. There are simple type forming operations A × B and A → B, as well as operations on dependent types, including in particular the sum x:A B(x) and product x:A B(x) types (see the appendix for details). The Curry-Howard interpretation of the operations A × B and A → B is as propositional conjunction and..
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Martin-Löf Complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.
Combinatorial Realizability Models of Type Theory.Pieter Hofstra & Michael A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):957-988.
Axiomatizations of Arithmetic and the First-Order/Second-Order Divide.Catarina Dutilh Novaes - forthcoming - Synthese.
Similar books and articles
Syntactic Calculus with Dependent Types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
A Note on Russell's Paradox in Locally Cartesian Closed Categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
An Intensional Type Theory: Motivation and Cut-Elimination.Paul C. Gilmore - 2001 - Journal of Symbolic Logic 66 (1):383-400.
Formal Semantics in Modern Type Theories with Coercive Subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.
Categorical and Algebraic Aspects of Martin-Löf Type Theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
Logicism and the Problem of Infinity: The Number of Numbers.G. Landini - 2011 - Philosophia Mathematica 19 (2):167-212.
An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics.Chris Fox & Shalom Lappin - 2004 - Logic Journal of the IGPL 12 (2):135-168.
First-Order, Curry-Typed Logic for Natural Language Semantics.Chris Fox, Shalom Lappin & Carl Pollard - unknown
Added to index2010-10-11
Total downloads59 ( #88,193 of 2,163,655 )
Recent downloads (6 months)4 ( #84,209 of 2,163,655 )
How can I increase my downloads?