Back to my publicationsNathaniel 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.
Last update: Tuesday, October 25, 2005 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)