(Developments Related to a Paper in ESOP 2016)

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs.A revised version of this paper has appeared in the

A specific benefit of the higher-order abstract syntax (HOAS) approach is that it allows substitutions to be treated at a meta-theoretic level. However, it is sometimes necessary to make substitutions over different kinds of expressions explicit. As a prelude to the rest of the development, we show here how this can be done while still deriving benefit from an HOAS treatment.

This section illustrates the use of the HOAS approach in defining transformations on functional programs. It does this by showing how the continuation-passing style, the closure conversion and the code hoisting transformations can be realized via λProlog programs in the context of the simply typed λ-calculus augmented with recursion.

This section provides the proof scripts in Abella that verify the implementations of the various transformations in λProlog. The initial subsections deal with library definitions and other related aspects that are common to the correctness proofs for the different transformations.

- util contains the some library definitions and theorems used in the main proofs.

- typing contains proofs for properties of evaluations in the source and target languages.

- eval contains proofs for properties of evaluations in the source and target languages.

- subst contains proofs for properties of explicit treatments of substitutions in the source and target languages. Most of the proofs are very concise because the actual substitutions are delegated to the meta language.

- cps_typ_pres contains the type preservation proof for the CPS transformation.
- cps_sem_pres contains the semantics preservation proof for the CPS transformation.

- cc_typ_pres contains the type preservation proof for the closure conversion.
- cc_sem_pres contains the semantics preservation proof for the closure conversion.

- ch_typ_pres contains the type preservation proof for the code hoisting.
- ch_sem_pres contains the semantics preservation proof for the code hoisting.

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.

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.