Higher-Order Abstract Syntax in Coq
Résumé
The terms of the simply-typed $\lambda$-calculus can be used to express the {\em higher-order abstract syntax} of objects such as logical formulas, proofs, and programs. Support for the manipulation of such objects is provided in several programming languages (e.g. $\lambda$Prolog, Elf). Such languages also provide embedded implication, a tool which is widely used for expressing {\em hypothetical judgments} in natural deduction. In this paper, we show how a restricted form of second-order syntax and embedded implication can be used together with induction in the Coq Proof Development system. We specify typing rules and evaluation for a simple functional language containing only function abstraction and application, and we fully formalize a proof of type soundness in the system. One difficulty we encountered is that expressing the higher-order syntax of an object-language as an inductive type in Coq generates a class of terms that contains more than just those that directly represent objects in the language. We overcome this difficulty by defining a predicate in Coq that holds only for those terms that correspond to programs. We use this predicate to express and prove the adequacy for our syntax.