Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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.

https://www.ps.uni-saarland.de/extras/types18/

Download PDF        Show BibTeX               

@CONFERENCE{SchaeferStark:2018:Embedding,
  title = {Embedding Higher-Order Abstract Syntax in Type Theory},
  author = {Steven Schäfer and Kathrin Stark},
  year = {2018},
  month = {Jun},
  booktitle = {24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18 - 21},
  pages = {69-71},
  address = {Braga, Portugal},
}

Login to edit