Verified Lisp and ML runtimes
Verified Lisp interpreters
The final case study in my PhD thesis was construction of verified machine-code implementations of Lisp on ARM, x86 and PowerPC. These initial implementations of a simple Lisp language (inspired by McCarthy's Lisp 1.5) were based on direct interpretation of the input expression. Such naive implementation strategies, of course, resulted in poor performance.
Verified Lisp implementation with dynamic compilation
Having finished the verified interpreters, Jared Davis contacted me and asked whether I could produce verified Lisp implementations that scale to the task of hosting his Milawa theorem prover. Milawa is a serious, resource-hungry Lisp program. With Jared guidance and some separate work on just-in-time compilation for x86, we managed to produce a verified Lisp implementation that dynamically compiles its input and is able to host the Milawa theorem prover. Later, we also proved that Milawa is sound when run on this verified implementation of Lisp.
Verified ML read-eval-print loop
Taking the above two projects further, Scott Owens, Ramana Kumar, Michael Norrish and I are working towards verified implementations of ML, for a subset of Standard ML that is meant to be both convenient to program in and clean enough to easily support formal reasoning about. For more about this project, see: cakeml.org.