Higher-Order Abstract Syntax with Induction in Coq

LPAR, pp. 159-173, 1994.

Cited by: 65|Bibtex|Views0|
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com
Keywords:
higher-order abstract syntaxtype systemlogical frameworksatisfiabilityhigher orderMore(2+)

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...More

Code:

Data:

Your rating :
0

 

Tags
Comments