Xavier Leroy's solution


A technical report describes the solution. The following remarks are copied from a message from Leroy to the POPLmark mailing list.

Some good things about this representation:

Some bad things about this representation:

One good thing about my solution: It is heavily commented, then typeset using the coqdoc tool. Message to my fellow solution submitters: you, too, can write good English; don't be shy.

One bad thing about my solution: My Coq proof scripts do not have the conciseness and elegance of Jérôme Vouillon's. Sorry, I've been using Coq for only 6 years...

Final thoughts: