Verified Compilation of Functional Programs
(Developments from the Thesis of Yuting Wang)


This website provides the code and the proof scripts that complement the material in the thesis of Yuting Wang entitled
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
that was submitted at the University of Minnesota in December 2016.

To run the code on this page, you will need to download the Teyjus implementation of λProlog. To run the proof scripts, you need to download the version of Abella that supports schematic polymorphism; this kind of polymorphism was introduced into Abella in the thesis.


Implementations of the Compiler for a Functional Language

This section illustrates the use of the HOAS approach in implementing a compiler for the simply typed λ-calculus augmented with recursion, conditionals and some built-in arithmetic operations. It does this by showing the continuation-passing style, the closure conversion, the code hoisting and code generation transformations can be realized via λProlog programs.


Verification of the Compiler for the Functional Language

This section provides the proof scripts in Abella that verify the implementation of the compiler in λProlog. The initial subsections deal with library definitions and other related aspects that are common to the correctness proofs for the different transformations. The following subsections deal with the correctness proof of individual transformations. The last subsection shows the combination of the individual correctness proofs to form the full correctness proof.

Some Library Definitions and Theorems

Properties of Typing

Properties of Evaluation

Properties of Substitutions

Verification of the CPS Transformation

Verification of the Closure Conversion Transformation

Verification of the Code Hoisting Transformation

Verification of the Code Generation Transformation

Correctness of the Full Compilation


The Complete Suite

The entire development can be downloaded as a tarball from here. Run 'make' command to compile the λProlog programs and the proof scripts. Make sure that the executables including the Teyjus compiler (tjcc) and linker (tjlink) and the Abella theorem prover (abella) are in the search path.


Acknowledgements

This material is based upon work supported by the National Science Foundation under Grant No CCF-0917140 and Grant No. CCF-1617771. The work has also received support from the University of Minnesota through a Doctoral Dissertation Fellowship and a Grant-in-Aid of Research. Any opinions, findings and conclusions or recommendations expressed in this material are those of the participants and do not necessarily reflect the views of the National Science Foundation.


The views and opinions expressed in this page are strictly those of the page author(s). The contents of this page have not been reviewed or approved by the University of Minnesota.