Verified LISP Implementations on ARM, x86 and PowerPC

Magnus O. Myreen, Michael J. C. Gordon
[doi] [Google Scholar] [DBLP] [Citeseer]

Theorem Proving in Higher Order Logics (TPHOLs)
Springer
Pages 359-374
2009
Note(s): Arm architecture, x86 architecture, PowerPC architecture, ISA specification, instruction set architecture