A Prototype Proof Translator from HOL to Coq
- 1 January 2000
- book chapter
- Published by Springer Nature
- p. 108-125
- https://doi.org/10.1007/3-540-44659-1_8
Abstract
No abstract availableKeywords
This publication has 5 references indexed in Scilit:
- Efficient representation and validation of proofsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Validation of HOL Proofs by Proof CheckingFormal Methods in System Design, 1999
- An interface between CLAM and HOLPublished by Springer Nature ,1998
- Hybrid interactive theorem proving using nuprl and HOLPublished by Springer Nature ,1997
- A comparative study of Coq and HOLPublished by Springer Nature ,1997