Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074381
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 3:11:29 PM
Last modification on : Saturday, January 27, 2018 - 1:30:56 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:15:54 PM

Identifiers

  • HAL Id : inria-00074381, version 1

Collections

Citation

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

Share

Metrics

Record views

117

Files downloads

313