Towards Higher-Order Abstract Syntax in Cedille (Work in Progress)

Abstract : 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 Cedille confirms we have a weakly initial algebra. Progress extending this to support dependent elimination is described.
Document type :
Conference papers
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download
Contributor : Ivan Scagnetto <>
Submitted on : Tuesday, June 11, 2019 - 2:28:48 PM
Last modification on : Thursday, June 13, 2019 - 11:32:35 AM


Files produced by the author(s)


  • HAL Id : hal-02152417, version 1



Aaron Stump. Towards Higher-Order Abstract Syntax in Cedille (Work in Progress). LFMTP 2019 Logical Frameworks and Meta-Languages: Theory and Practice 2019, Jun 2019, Vancouver, Canada. ⟨hal-02152417⟩



Record views


Files downloads