This page contains information about work related to implementing compilers for functional languages using the Teyjus implementation of λProlog and verifying such implementations using the Abella interactive theorem-prover. These systems seem 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 the systems support.
The experiments described here have concerned the simply typed λ-calculus extended with recursion and some simple built-in operations. The results have been quite illuminating. We have been able to cleanly implement and verify key transformations such as the cps transformation, closure conversion and code hoisting. The implementations benefit from higher-order abstract syntax representations. For example, we utilize 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 derive benefit from a higher-order representation in encoding and using the step-indexed logical relation that is needed in our correctness proof. This relation has to be extended to open terms under equivalent substitutions. The treatment of substitutions in the definition of this relation and in the proofs based on the definition use β-conversion together with concepts such as nominal constants and nominal abstraction that are present in Abella.
This website provides the code and the proof scripts for some of the case studies we have conducted, including the cps, closure conversion and code hoisting transformations described above. As such, it complements the material in the paper A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, by Yuting Wang and Gopalan Nadathur that has been accepted for presentation at the 2016 European Symposium on Programming. To run the code on this page, you will need to download the Teyjus implementation. To run the proof scripts, you need to download Version 2.0.2 of the Abella system.
The structure of the code and proof developments to be found in this website is explained below.
The following example shows how an explicit representation of substitutions can be provided and reasoned about elegantly by using HOAS in Abella.
The following are the implementations of transformations in λProlog
The following provide verifications in Abella of different aspects related to the implementations of transformations provided earlier
This work has been partially supported by the National Science Foundation grant CCF-0917140. It has also received support from the University of Minnesota through a Doctoral Dissertation Fellowship and a Grant-in-Aid of Research. Opinions, findings and conclusions or recommendations that are manifest in this material are those of the participants and do not necessarily reflect the views of the NSF.