Higher-order abstract syntax in Coq
- 1 January 1995
- book chapter
- Published by Springer Nature
- p. 124-138
- https://doi.org/10.1007/bfb0014049
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- A logic programming approach to implementing higher-Order term rewritingPublished by Springer Nature ,2005
- Natural semantics and some of its meta-theory in ElfPublished by Springer Nature ,2005
- Compiler verification in LFPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A framework for defining logicsJournal of the ACM, 1993
- Implementing tactics and tacticals in a higher-order logic programming languageJournal of Automated Reasoning, 1993
- Using typed lambda calculus to implement formal systems on a machineJournal of Automated Reasoning, 1992
- From operational semantics to abstract machinesMathematical Structures in Computer Science, 1992
- Implementing the meta-theory of deductive systemsPublished by Springer Nature ,1992