Graduate studies at Western
|Abstract||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)|
No categories specified
(categorize this paper)
|Through your library||Only published papers are available at libraries|
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 & Carl Pollard, First-Order, Curry-Typed Logic for Natural Language Semantics.
Added to index2010-10-11
Total downloads22 ( #62,693 of 725,973 )
Recent downloads (6 months)1 ( #61,087 of 725,973 )
How can I increase my downloads?