Preprint
Elaborating Inductive Definitions and Course-of-Values Induction in Cedille
ArXiv.org
03/19/2019
DOI: 10.48550/arxiv.1903.08233
Abstract
In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style
type theory, it is possible to generically {\lambda}-encode inductive datatypes
which support course-of-values (CoV) induction. We present a datatype subsystem
for Cedille (an implementation of CDLE) that provides this feature to
programmers through convenient notation for declaring datatypes and for
defining functions over them by case analysis and fixpoint-style recursion
guarded by a type-based termination checker. We demonstrate that this does not
require extending CDLE by showing how datatypes and functions over them
elaborate to {\lambda}-encodings, and proving that this elaboration is type-
and value-preserving. This datatype subsystem and elaborator are implemented in
Cedille, establishing for the first time a complete translation of inductive
definitions to a small pure typed {\lambda}-calculus.
Details
- Title: Subtitle
- Elaborating Inductive Definitions and Course-of-Values Induction in Cedille
- Creators
- Christopher JenkinsColin McDonaldAaron Stump
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.1903.08233
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 03/19/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984410848302771
Metrics
3 Record Views