This week’s tech talk will be Magnus Myreen from Cambridge talking about mechanically verified Lisp interpreters. It will be held at the irregular time of 2pm, Friday Nov 14.
This talk describes work on constructing verified interpreters for a small LISP-like language using the interactive theorem prover HOL4. The LISP interpreters have been proved correct with respect to detailed x86, ARM and PowerPC processor models (written by Sarkar, Fox and Leroy). New techniques for expressing correctness of machine code were developed, as well as new techniques for proof-producing decompilation and compilation to/from HOL4 functions. A copying garbage collector (a Cheney collector) was verified and subsequent proofs were built upon its verified specification.