A verified runtime for a verified theorem prover

Magnus O. Myreen, Jared Davis
[ISBN] [Google Scholar] [DBLP] [Citeseer]

Interactive Theorem Proving
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 265-280
2011
Note(s): ISA specification, compiler verification