Abstract
We describe a low-level proof format, which can be used for independent proof checking and as an intermediate language for translating proofs between systems. The checker is presented as a virtual machine and the proof format as the bytecode. We compare HOL and Coq with a view to designing this pivot language, and describe a prototype which converts recorded HOL proofs into this intermediate format, and then translates them into Coq.
Cite
CITATION STYLE
Denney, E. (2000). A prototype proof translator from hol to coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 108–125). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
