A locally nameless solution to the POPLmark challenge

It is written in Coq and uses a ``locally nameless'' representation for binders: variables bound within terms are represented by de Bruijn indices, but variables free in terms are represented by names. This representation is described in more details in Randy Pollack's talk, Reasoning About Languages with Binding.

• Technical report documenting the solution, in literate programming style.

• The Coq source files: in a .tar.gz archive, or as individual files:
  • extralibrary.v (various auxiliary lemmas and tactics).
  • part1a.v (the solution to part 1A of the challenge: algorithmic subtyping).
  • part2a.v (the solution to part 2A of the challenge: type soundness).
  • part3.v (the solution to part 3 of the challenge: execution of the semantics).