A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, inductive datatypes with their induction principles are derived. One benefit of this approach is that it allows exploratio...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-10-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1910.10851v1 |