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.
Type de document :
RR-2556, INRIA. 1995
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:34:07
Dernière modification le : jeudi 11 janvier 2018 - 16:41:52
Document(s) archivé(s) le : jeudi 24 mars 2011 - 14:17:36



  • 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〉



Consultations de la notice


Téléchargements de fichiers