[POPLmark] Comparison of certified code transformations for functional languages?
Adam Chlipala
adamc at cs.berkeley.edu
Sat May 12 22:07:16 EDT 2007
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.
More information about the Poplmark
mailing list