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

[Adam Chlipala]

I'm looking for examples of compiler-like code transformations on 
statically-typed functional programming languages, with mechanized type 
preservation and semantics preservation proofs.  I'm trying to come up 
with some objective evidence that the toolkit I've been developing 
(http://ltamer.sourceforge.net/) supports effective engineering of these 
kinds of proofs.  [I talked about an early version of this at the last 
MM workshop.]

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.  Still, it provides some 
starting point for comparison, so I implemented a similar example in Coq 
(including a semantics preservation proof) using my library for PL 
mechanization.

A pretty-printed HTML version with comments:
	http://ltamer.sourceforge.net/coq/examples.CPS.html

The actual source file: 
http://ltamer.cvs.sourceforge.net/ltamer/ltamer/examples/CPS.v?revision=1.5

The main difference is that I use 'bool' as the base type instead of 
'unit', since the original choice leaves every type inhabited by exactly 
one value, up to extensional equivalence.  With the denotational 
approach I use, that would make the semantics preservation theorem 
provable by a trivial argument independent of the actual CPS transform.

Can anyone point me to anything else that would make sense to compare 
with?  Or you can think of this as another, vaguely-specified challenge 
problem. ;-)