Publication details

Saarland University Computer Science

Embedding Higher-Order Abstract Syntax in Type Theory

Steven Schäfer, Kathrin Stark

24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18 - 21, pp. 69-71, June 2018

Higher-order abstract syntax (HOAS) offers a direct representation of higher-order languages, where capture-avoiding substitution is function application, substitution lemmas hold by definition and all derived constructions respect substitution. However, embedding HOAS directly into type theory (and thus profiting from its perks) is difficult, since HOAS relies on an intensional host language function space, while type theoretic function spaces are extensional. We propose an indirect approach via presheaf models.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy