Building Reliable Compilers with a Formal Methods Framework.

Nathaniel Gray, Cristian Tapus, Aleksey Nogin, and Jason Hickey.
Building Reliable Compilers with a Formal Methods Framework.
In Dr. Indrakshi Ray, editor, The 14th International Symposium on Software Reliability Engineering (ISSRE 2003). Sumpplementary Proceeding, pages 319–320. Chillarege Press, 2003.
PDF, PostScript.

Abstract

We present a new approach to building reliable compilers. By implementing a compiler in a general-purpose logical framework (MetaPRL) we are able to reduce dramatically the amount of trusted code and provide a semi-formal specification of the compiling stages. This simplifies the design of the compiler and it could allow for formal reasoning about the correctness of compiled programs.