Nathaniel Gray, Jason Hickey, Aleksey Nogin, and Cristian Tapus
Building extensible compilers in a formal framework. A formal framework user's perspective.
In Konrad Slind, editor, Emerging Trends. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), pages 57--70. University of Utah, 2004.
PDF (234KB), PostScript (368KB)
We outline a new methodology for compiler design, based on the use of a transformation logic defined within an existing general-purpose logical framework. We discuss how this methodology can be used to address several central issues in compiler design and implementation: ease of implementation, extensibility, compositionality, and trust. We show how pre-existing features of the logical framework we use help in compiler implementation; and we also discuss which features need to be added to the framework in order to facilitate our approach to compiler development.
Back to my publications
Last update: Tuesday, October 25, 2005 by Aleksey Nogin (e-mail: email@example.com)