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