A Caltech Library Service

High-Confidence, Modular Compiler Development in a Formal Environment


Gray, Nathaniel Asoka (2005) High-Confidence, Modular Compiler Development in a Formal Environment. Master's thesis, California Institute of Technology. doi:10.7907/RBAD-VH06.


We present a methodology for realistic compiler development in an existing formal methods framework. Program transformations and analyses are implemented as term rewrites and inference rules, and automated proof search techniques are used to drive the compilation process. This approach allows the programmer to implement the compiler succinctly, declaratively, and modularly. We explain how our methodology separates trusted code, which can potentially corrupt compilation, from untrusted code, which cannot. We present a case study in which we have used these techniques to implement a compiler for a small ML-like programming language that produces x86 assembly code as output. We give a detailed overview of several stages of the compiler, including type inference, type checking, type erasure, CPS conversion, and closure conversion. We also describe the process of extending the minimal core compiler to include features such as integers, Booleans, operators, tuples, and recursive functions.

Item Type:Thesis (Master's thesis)
Subject Keywords:compiler verification; compilers; formal compilers; formal toolkits; meta-prl; metaprl; theorem provers
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Hickey, Jason J.
Thesis Committee:
  • Unknown, Unknown
Defense Date:3 June 2005
Record Number:CaltechETD:etd-05272005-182952
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:2164
Deposited By: Imported from ETD-db
Deposited On:05 Jun 2005
Last Modified:07 May 2020 22:43

Thesis Files

PDF - Final Version
See Usage Policy.


Repository Staff Only: item control page