Journal article
The calculus of dependent lambda eliminations
Journal of functional programming, Vol.27, E14
2017
DOI: 10.1017/S0956796817000053
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.
Details
- Title: Subtitle
- The calculus of dependent lambda eliminations
- Creators
- AARON Stump - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Journal of functional programming, Vol.27, E14
- Publisher
- Cambridge University Press
- DOI
- 10.1017/S0956796817000053
- ISSN
- 0956-7968
- eISSN
- 1469-7653
- Number of pages
- 41
- Language
- English
- Date published
- 2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984259471002771
Metrics
7 Record Views