Journal article
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Electronic Proceedings in Theoretical Computer Science, Vol.307(Proc. LFMTP 2019), pp.55-67
10/23/2019
DOI: 10.4204/EPTCS.307.6
Abstract
EPTCS 307, 2019, pp. 55-67 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 exploration of new or
advanced forms of inductive datatypes. This paper reports work in progress on
one such form, namely higher-order abstract syntax (HOAS). We consider the
nature of HOAS in the setting of pure type theory, comparing with the
traditional concept of environment models for lambda calculus. We see an
alternative, based on what we term Kripke function-spaces, for which we can
derive a weakly initial algebra in Cedille. Several examples are given using
the encoding.
Details
- Title: Subtitle
- A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
- Creators
- Aaron Stump - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Electronic Proceedings in Theoretical Computer Science, Vol.307(Proc. LFMTP 2019), pp.55-67
- DOI
- 10.4204/EPTCS.307.6
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Language
- English
- Date published
- 10/23/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259408002771
Metrics
13 Record Views