A comparative study of Coq and HOL
- 1 January 1997
- book chapter
- Published by Springer Nature
- p. 323-337
- https://doi.org/10.1007/bfb0028403
Abstract
No abstract availableKeywords
This publication has 15 references indexed in Scilit:
- Translating dependent type theory into higher order logicPublished by Springer Nature ,2005
- A mechanisation of computability theory in HOLPublished by Springer Nature ,1996
- Function definition in higher-order logicPublished by Springer Nature ,1996
- Inductive definitions: Automation and applicationPublished by Springer Nature ,1995
- Automatically synthesized term denotation predicates: A proof aidPublished by Springer Nature ,1995
- Extracting text from proofsPublished by Springer Nature ,1995
- Developing certified programs in the system Coq the program tacticPublished by Springer Nature ,1994
- A HOL package for reasoning about relations defined by mutual inductionPublished by Springer Nature ,1994
- Synthesis of ML programs in the system CoqJournal of Symbolic Computation, 1993
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940