The calculus of dependent lambda eliminations*. (9th May 2017)

• Record Type: Journal Article
• Authors: STUMP, AARON
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2017-05-09
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796817000053
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.