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

[Francois Pottier]

Hello,

This is a reply to Adam's question. I have written a (quite simplistic)
version of closure conversion using my prototype implementation of Pure
FreshML. Neither type preservation nor semantic preservation are proved;
however, the property that names are properly bound (so closed terms are
mapped to closed terms) is automatically checked. The code is at

  http://cristal.inria.fr/~fpottier/freshml/sample/cc.fml

and a paper that describes Pure FreshML (to appear at LICS'07) can be found at

  http://cristal.inria.fr/~fpottier/publis/fpottier-pure-freshml.pdf

Best regards,

-- 
François Pottier
Francois.Pottier at inria.fr
http://cristal.inria.fr/~fpottier/