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

[Xavier Leroy]

> I'm looking for examples of compiler-like code transformations on
> statically-typed functional programming languages, with mechanized type
> preservation and semantics preservation proofs.  [...]
> The closest thing I've found outside my own work is this:
> 	http://twelf.plparty.org/wiki/CPS_conversion
> ...which is a CPS transform for simply-typed lambda calculus,
> implemented in Twelf with a proof of type preservation but no dynamic
> semantics or proof of semantics preservation.

Here are two other examples of mechanized proofs of semantics preservation
for CPS translations:

[1] "Verifying CPS Transformations in Isabelle/HOL"
    Yasuhiko Minamide Koji Okuma
    http://www.score.is.tsukuba.ac.jp/~minamide/papers/merlin03.pdf

[2] "Mechanically verifying correctness of CPS compilation"
    Ye Henry Tian 	
    http://crpit.com/confpapers/CRPITV51Tian.pdf

There are several flavors of CPS translation, depending on whether
administrative redexes are eliminated on the fly or not.  While the
naive CPS translation can be proved correct using a nominal approach
without alpha-conversion (as in the first part of [1]), the more
optimized translations need proper handling of binders.  [1] uses
names and definitions modulo explicit alpha-conversion, while [2] uses
HOAS.

Other transformations relevant to the compilation of functional
languages include:

- Closure conversion.  Proving semantics preservation in an untyped
  setting is not really hard, but in a typed setting you need
  existential types in the target language.

- Uncurrying, i.e. transforming curried functions to N-ary functions.
  For those who can read French, my PhD student Zaynah Dargaye
  wrote a short paper on her Coq proof of correctness for an
  uncurrying transformation similar to that used in the OCaml native
  compiler:
     http://gallium.inria.fr/~dargaye/publications/certdec.pdf

Best wishes,

- Xavier