# Higher-Order Abstract Syntax in Coq

1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Keywords :
Type de document :
Rapport
RR-2556, INRIA. 1995
Domaine :

https://hal.inria.fr/inria-00074124
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

### Identifiants

• HAL Id : inria-00074124, version 1

### Citation

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

### Métriques

Consultations de la notice

## 105

Téléchargements de fichiers