Citation
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. https://resolver.caltech.edu/CaltechETD:etd-05272005-182952
Abstract
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): |
|
Thesis Committee: |
|
Defense Date: | 3 June 2005 |
Record Number: | CaltechETD:etd-05272005-182952 |
Persistent URL: | https://resolver.caltech.edu/CaltechETD:etd-05272005-182952 |
DOI: | 10.7907/RBAD-VH06 |
Default Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. |
ID Code: | 2164 |
Collection: | CaltechTHESIS |
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. 405kB |
Repository Staff Only: item control page