Book chapter
Impredicative Encodings of Inductive-Inductive Data in Cedille
Trends in Functional Programming, pp.1-15
Lecture Notes in Computer Science, v. 13868, Springer Nature Switzerland
08/28/2023
DOI: 10.1007/978-3-031-38938-2_1
Abstract
Cedille is a dependently typed programming language known for expressive and efficient impredicative encodings. In this work, we show that encodings of induction-induction are also possible by employing a standard technique from other encodings in Cedille, where a type representing the shape of data is intersected with a predicate that further constrains. Thus, just as with indexed inductive data, Cedille can encode a notion that is often axiomatically postulated or directly implemented in other dependent type theories without sacrificing efficiency.
Details
- Title: Subtitle
- Impredicative Encodings of Inductive-Inductive Data in Cedille
- Creators
- Andrew Marmaduke - University of IowaLarry Diehl - University of IowaAaron Stump - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Trends in Functional Programming, pp.1-15
- Publisher
- Springer Nature Switzerland; Cham
- Series
- Lecture Notes in Computer Science; v. 13868
- DOI
- 10.1007/978-3-031-38938-2_1
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 08/28/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984458109502771
Metrics
1 Record Views