HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Higher-Order Abstract Syntax in Coq

Abstract : 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:34:07 PM
Last modification on : Friday, February 4, 2022 - 3:18:44 AM
Long-term archiving on: : Thursday, March 24, 2011 - 2:17:36 PM


  • HAL Id : inria-00074124, version 1



Joëlle Despeyroux, Amy Felty, André Hirschowitz. Higher-Order Abstract Syntax in Coq. RR-2556, INRIA. 1995. ⟨inria-00074124⟩



Record views


Files downloads