Conference proceeding
Generic derivation of induction for impredicative encodings in Cedille
Proceedings of the 7th ACM SIGPLAN International Conference on certified programs and proofs, Vol.2018-, pp.215-227
CPP 2018
01/08/2018
DOI: 10.1145/3167087
Abstract
This paper presents generic derivations of induction for impredicatively typed lambda-encoded datatypes, in the Cedille type theory. Cedille is a pure type theory extending the Curry-style Calculus of Constructions with implicit products, primitive heterogeneous equality, and dependent intersections. All data erase to pure lambda terms, and there is no built-in notion of datatype. The derivations are generic in the sense that we derive induction for any datatype which arises as the least fixed point of a signature functor. We consider Church-style and Mendler-style lambda-encodings. Moreover, the isomorphism of these encodings is proved. Also, we formalize Lambek's lemma as a consequence of expected laws of cancellation, reflection, and fusion.
Details
- Title: Subtitle
- Generic derivation of induction for impredicative encodings in Cedille
- Creators
- Denis Firsov - University of IowaAaron Stump - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 7th ACM SIGPLAN International Conference on certified programs and proofs, Vol.2018-, pp.215-227
- Series
- CPP 2018
- DOI
- 10.1145/3167087
- Publisher
- ACM
- Grant note
- DOI: 10.13039/100000001, name: National Science Foundation, award: 1524519; name: Department of Defense, award: FA9550-16-1-0082
- Language
- English
- Date published
- 01/08/2018
- Academic Unit
- Computer Science
- Record Identifier
- 9984259437202771
Metrics
3 Record Views