David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
S. Awodey & M. A. Warren (2013). Martin-Löf Complexes. Annals of Pure and Applied Logic 164 (10):928-956.
Pieter Hofstra & Michael A. Warren (2013). Combinatorial Realizability Models of Type Theory. Annals of Pure and Applied Logic 164 (10):957-988.
Similar books and articles
Aarne Ranta (1998). Syntactic Calculus with Dependent Types. Journal of Logic, Language and Information 7 (4):413-431.
Andrew M. Pitts & Paul Taylor (1989). A Note on Russell's Paradox in Locally Cartesian Closed Categories. Studia Logica 48 (3):377 - 387.
Paul C. Gilmore (2001). An Intensional Type Theory: Motivation and Cut-Elimination. Journal of Symbolic Logic 66 (1):383-400.
Zhaohui Luo (2012). Formal Semantics in Modern Type Theories with Coercive Subtyping. Linguistics and Philosophy 35 (6):491-513.
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.
G. Landini (2011). Logicism and the Problem of Infinity: The Number of Numbers. Philosophia Mathematica 19 (2):167-212.
Chris Fox & Shalom Lappin (2004). An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics. Logic Journal of the Igpl 12 (2):135-168.
Chris Fox, Shalom Lappin & Carl Pollard, First-Order, Curry-Typed Logic for Natural Language Semantics.
Added to index2010-10-11
Total downloads25 ( #81,095 of 1,688,130 )
Recent downloads (6 months)2 ( #112,061 of 1,688,130 )
How can I increase my downloads?