Another semantic solution to the 2nd List-machine Benchmark

A high-level language compilation challenge problem

A compilation from pure Fsub to the Calculus of Constructions

This Coq code implements a translation of pure Fsub types and terms into Coq's own logic. The translation is proved to respect the evaluation relation from the POPLmark challenge. Composing the translation with Coq's extraction mechanism and the OCaml native code compiler, we get a compiler from Fsub terms to native code. If we trust extraction and the OCaml compiler, then we have a certified compiler. Since the Calculus of Constructions has been proved safe and strongly normalizing, the existence of the translation ought to be some kind of proof that pure Fsub is safe and strongly normalizing, though the details are murky.

POPLmark Challenge Part 1A solution

Here's my solution, which uses a locally nameless encoding in Coq. In comparison to other solutions using proof assistants, I've tried to write mine so that the entire thing is readable and informative for humans, including proof scripts. (That fact that I've tried doesn't mean that I've succeeded. ;-))

The solution is divided into two pieces: a re-usable library about contexts and the part specific to the challenge problem. I haven't expended any great effort in making the library part pleasant to read. I don't think anything in it corresponds to anything described explicitly in the formal development of the POPLmark Challenge paper's appendix, and the theorems in it should apply to a wide range of PL developments, so I think it's fair to evaluate the main solution file separately.

A good portion of the definitions in the main file would ideally be generated automatically by a tool in the spirit of the Isabelle nominal logic extension. I've indicated with comments which I think these are.