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
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 265-280
2011
Note(s): ISA specification, compiler verification