11. Where HOAS Is Native🔗

Naive HOAS fails in Lean for two separate reasons: as an inductive type it would make the logic inconsistent, and Lean's functions are rich enough to build exotic terms. Logical frameworks avoid both. There, lam : (tm → tm) → tm is a declared constant rather than an inductive type with recursion over it, and the framework's functions contain only λ-terms. Naive HOAS is then sound and adequate: object terms correspond one-to-one to framework terms in normal form.

• Twelf: the LF logical framework with a logic programming engine for metatheory.

• Beluga: contextual types let programs pattern-match on HOAS terms together with their contexts.

• Abella: a two-level logic whose ∇ quantifier reasons about fresh names.

• λProlog: higher-order logic programming, with HOAS as its native idiom.

Further reading: Pfenning and Elliott, Higher-Order Abstract Syntax (1988); Chlipala, Parametric Higher-Order Abstract Syntax for Mechanized Semantics (2008); Chlipala, Certified Programming with Dependent Types, chapter on higher-order syntax.