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

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 3:11:29 PM
Last modification on : Friday, February 4, 2022 - 3:18:43 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:15:54 PM


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



Record views


Files downloads