A Caltech Library Service

Compiler implementation in a formal logical framework

Hickey, Jason and Nogin, Aleksey and Granicz, Adam (2003) Compiler implementation in a formal logical framework. In: MERLIN '03 Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding. ACM , New York, NY. ISBN 1-58113-800-8.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


he task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using the MetaPRL logical framework to compile an ML-like language to Intel x86 assembly. We also present a scoped formalization of x86 assembly in which all registers are immutable.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Additional Information:© 2003 ACM. Additional Author: Brian Aydemir. This work was supported in part by the DoD Multidisciplinary University Research Initiative (MURI) program administered by the Office of Naval Research (ONR) under Grant N00014-01-1-0765, the Defense Advanced Research Projects Agency (DARPA), the United States Air Force, the Lee Center, and by NSF Grant CCR 0204193.
Funding AgencyGrant Number
Office of Naval Research (ONR)N00014-01-1-0765
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Caltech Lee Center for Advanced NetworkingUNSPECIFIED
Subject Keywords:Reliability, Verification, Formal compiler, higher-order abstract syntax, logical programming environment
Classification Code:D.3.4 [ Programming Languages ]: Processors— Translator writing systems and compiler generators ; D.2.4 [ Software Engineering ]: Software/Program Verification— Formal methods
Record Number:CaltechAUTHORS:20161102-171842275
Persistent URL:
Official Citation:Jason Hickey, Aleksey Nogin, and Adam Granicz. 2003. Compiler implementation in a formal logical framework. In Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding (MERLIN '03). ACM, New York, NY, USA, 1-13. DOI=
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:71704
Deposited On:03 Nov 2016 16:55
Last Modified:11 Nov 2021 04:49

Repository Staff Only: item control page