[POPLmark] Comparison of certified code transformations for functional languages?

[Stefan Monnier]

> The closest thing I've found outside my own work is this:
> 	http://twelf.plparty.org/wiki/CPS_conversion

We're working on a type-preserving compiler here, written in Haskell and
using GHC's GADTs to encode the type preservation proof.  We had a paper in
PLPV'06 showing how it worked for the CPS conversion
(http://www.iro.umontreal.ca/~monnier/tct.pdf).  It has now been extended to
closure conversion and hoisting, but the corresponding article is still
being written.

We do not attempt to cover semantics preservation, tho, only
type-preservation.


        Stefan