Book chapter
Project Report: Dependently Typed Programming with Lambda Encodings in Cedille
Trends in Functional Programming, pp.115-134
Lecture Notes in Computer Science, Springer International Publishing
02/21/2019
DOI: 10.1007/978-3-030-14805-8_7
Abstract
This project report presents Cedille, a dependent type theory based on lambda encodings. Cedille is an extension of the Calculus of Constructions with new type features enabling induction and large eliminations (computing a type by recursion on a term) for lambda encodings, which are not available for lambda-encoded data in related type theories. Cedille is presented through a number of examples, including both programs and proofs.
Details
- Title: Subtitle
- Project Report: Dependently Typed Programming with Lambda Encodings in Cedille
- Creators
- Ananda Guneratne - University of IowaChad Reynolds - University of IowaAaron Stump - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Trends in Functional Programming, pp.115-134
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-14805-8_7
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 02/21/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259485902771
Metrics
10 Record Views