Verified Compilation of Functional Programs

This page provides information about an ongoing project at the University of Minnesota that is related to implementing compilers for functional languages using the λProlog language and verifying these implementations using the Abella interactive theorem-prover. The thesis underlying this work is that these systems are well-suited to this application: transformations on functional programs involves manipulating and reasoning about binding structure in interesting ways, something that is done well using the particular brand of higher-order abstract syntax (called λ-tree syntax) that both λProlog and Abella support.

The experiments conducted thus far have focused on the simply typed λ-calculus extended with recursion and some simple built-in operations. The results that we have obtained in this domain have been quite promising. We have been able to cleanly implement and verify key transformations such as the cps transformation, closure conversion and code hoisting. The implementations have benefitted from higher-order abstract syntax representations. For example, we have utilized such a representation in an intrinsic way in calculating the free variables in a function and in later structuring the closure conversion transformation based on this calculation. As another example, we have derived benefit from a higher-order representation in encoding and using the step-indexed logical relations that are often used in our correctness proofs. These relation have typically to be extended to open terms under equivalent substitutions. The treatment of substitutions in the definition of such relations and in the proofs based their definition use to advantage the understanding of β-conversion together with concepts such as nominal constants and nominal abstraction that is present in Abella.

Specific details about the results that have been obtained up to this point can be found in the following places:

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.