vai al contenuto della pagina vai al menu di navigazione

Lambda Types on the Lambda Calculus with Abbreviations

F. Guidi


University of Bologna (Italy). Department of Computer Science.

The author presents lambda-delta, a lambda-typed lambda calculus with a single lambda binder and abbreviations. This calculus pursues the reuse of the term constructions both at the level of types and at the level of contexts as the main goal. Up to reduction lambda-delta shares with Church simply typed lambda calculus the subset of typable terms but in the "propositions as types" perspective it can encode the implicative fragment of predicative logic without quantifiers because dependent types are allowed. lambda-delta enjoys the properties of Church simply typed lambda calculus (mainly subject reduction, strong normalization and decidability of type inference) and, in addition, it satisfies the correctness of types and the uniqueness of types up to reduction. We stress that technically lambda-delta differs from the Automath-related lambda calculi in that they do not provide for an abbreviation construction at the level of terms. Moreover lambda-delta features a type hierarchy with an infinite number of levels both above and below any reference point.