Higher-order abstract syntax with induction in Coq

Joëlle Despeyroux 1 André Hirschowitz 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Three important properties of Higher-Order Abstract Syntax are the (higher-order) induction principle, which allows proofs by induction, the (higher-order) injection principle, which asserts that equal terms have equal heads and equal sons, and the extensionality principle, which asserts that functional terms which are pointwise equal are equal. Higher-order abstract syntax is implemented for instance in the Edinburgh Logical Framework and the above principles are satisfied by this implementation. But although they can be proved at the meta level, they cannot be proved at the object level and furthermore, it is not so easy to know how to formulate them in a simple way at the object level. We explain here how Second-Order Abstract Syntax can be implemented in a more powerful type system (Coq) in such a way as to make available or provable (at the object level) the corresponding induction, injection and extensionality principles.
Type de document :
[Research Report] RR-2292, INRIA. 1994
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:11:29
Dernière modification le : samedi 27 janvier 2018 - 01:30:56
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:15:54



  • HAL Id : inria-00074381, version 1



Joëlle Despeyroux, André Hirschowitz. Higher-order abstract syntax with induction in Coq. [Research Report] RR-2292, INRIA. 1994. 〈inria-00074381〉



Consultations de la notice


Téléchargements de fichiers