Higher-Order Abstract Syntax with induction in Coq
- 1 January 1994
- book chapter
- Published by Springer Nature
- p. 159-173
- https://doi.org/10.1007/3-540-58216-9_36
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- Elf: a language for logic definition and verified metaprogrammingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Compiler verification in LFPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Higher-Order Abstract Syntax with induction in CoqPublished by Springer Nature ,1994
- Implementing the meta-theory of deductive systemsPublished by Springer Nature ,1992
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- Higher-order abstract syntaxPublished by Association for Computing Machinery (ACM) ,1988