Lambda Types on the Lambda Calculus with Abbreviations

for an informal presentation at CIE 2007 [2] is a typed -calculus that pursues the reuse of the term constructions both at the level of types and at the level of contexts, while enjoying the most common metatheoretical properties [1]. Notice that the distinction we are making here between terms and types is borrowed from the simply typed -calculus . The development of is intended as the first step towards the verification of the following conjecture: the adoption of a single set of constructions for terms, types, and contexts (i.e. the "contexts as types as terms" paradigm) is compatible with the presence of a desirable meta-theory. features the term constructions of Church plus sorts, abbreviations and type casts. Sorts are necessary to build closed terms, abbreviations (i.e. let expressions) are essential in the proofs of some meta-theoretical properties when the "types as terms" paradigm is adopted and are practically unavoidable in mathematics and computer sc...

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: F. Guidi
• Keywords: Common Metatheoretical Properties, Constructions, CORR 2006, Education, Paradigm