Home > lambdatheultimate > Formal Compiler Implementation in a Logical Framework

Formal Compiler Implementation in a Logical Framework

June 8th, 2010 06:11 admin Leave a comment Go to comments

Hickey, Jason and Nogin, Aleksey and Granicz, Adam and Aydemir, Brian (2003) Formal Compiler Implementation in a Logical Framework. Technical Report. California Institute of Technology.

The 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.

I don’t understand the details of this paper, but the general approach of using rewriting for compilation (including passes such as closure conversion) is very interesting in itself.

(Edit: As a bonus, the paper is derived from the literate MetaPRL sources.)

Source: Formal Compiler Implementation in a Logical Framework

Related Articles:

  1. MELT, a GCC Compiler Plugin Framework, Reaches 1.0
  2. When Formal Systems Kill: Computer Ethics and Formal Methods
  3. A Monadic Framework for Delimited Continuations
  4. The marriage of bisimulations and Kripke logical relations
  5. The marriage of bisimulations and Kripke logical relations
blog comments powered by Disqus
YOYOYOOYOYOYO