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

[Adam Chlipala]

Karl Crary wrote:
> By the way, why can't the POPLmark challenge serve for an 
> apples-to-apples comparison?  It was certainly intended to.

Yes, but it only dealt with certain kinds of proofs.  There seem to be 
different issues surrounding mechanized proofs about code 
transformations, and I'd like to understand how that affects choice of 
tools and libraries.  Also, the original challenge focused on a type 
soundness proof, but there are some formalization techniques where such 
results are implicit (like the one I've been using).  That's a big 
reason why I'm interested in results that aren't "automatic" in that 
kind of setting.