Journal article
Efficient lambda encodings for Mendler-style coinductive types in Cedille
Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol.317, pp.72-97
04/30/2020
DOI: 10.4204/EPTCS.317.5
Abstract
EPTCS 317, 2020, pp. 72-97 In the calculus of dependent lambda eliminations (CDLE), it is possible to
define inductive datatypes via lambda encodings that feature constant-time
destructors and a course-of-values induction scheme. This paper begins to
address the missing derivations for the dual, coinductive types. Our derivation
utilizes new methods within CDLE, as there are seemingly fundamental
difficulties in adapting previous known approaches for deriving inductive
types. The lambda encodings we present implementing coinductive types feature
constant-time constructors and a course-of-values corecursion scheme.
Coinductive type families are also supported, enabling proofs for many standard
coinductive properties such as stream bisimulation. All work is mechanically
verified by the Cedille tool, an implementation of CDLE.
Details
- Title: Subtitle
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- Creators
- Christopher JenkinsAaron Stump - University of IowaLarry Diehl
- Resource Type
- Journal article
- Publication Details
- Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol.317, pp.72-97
- DOI
- 10.4204/EPTCS.317.5
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Language
- English
- Date published
- 04/30/2020
- Academic Unit
- Computer Science
- Record Identifier
- 9984259477102771
Metrics
8 Record Views