[TYPES] HOAS Techniques in Verified Transformations on Functional Programs

[Yuting Wang]

Verified Transformations on Functional Programs Using
           Higher-Order Abstract Syntax Techniques

I would like to announce the work that I have been doing as part
of my doctoral thesis to bring out the benefits of higher-order
abstract syntax methods in implementing and verifying compiler
transformations commonly used for functional programming
languages. Transformations such as closure conversion and code
hoisting have to pay special attention to binding structure, an
aspect that is given a meta-level treatment in systems such as
Abella, Beluga, Twelf and Lambda Prolog. In collaborative work
with Gopalan Nadathur that will be presented at ESOP 2016, we
have shown how the devices present in Lambda Prolog and Abella,
two systems developed collaboratively by our group at the
University of Minnesota and the Parsifal group at Inria-Saclay,
can used to provide succinct implementations and clear formal
proofs for the correctness of these transformations in the
context of a representative functional language. The
implementation, proofs and accompanying paper are available at
the following URL:

http://www-users.cs.umn.edu/~yuting/compilation/index.html

I would appreciate any comments you might have about the code and the
proofs and would also be happy to answer any questions that arise as
you look at the material.

Best,
- Yuting


-- 
Yuting Wang <yuting at cs.umn.edu>
University of Minnesota, Dept. of Computer Science
http://www.cs.umn.edu/~yuting