A locally nameless solution to the POPLmark challenge

This is a solution to the POPLmark challenge. Originally, only part 1A (properties of subtyping) of the challenge was addressed; now, it also addresses parts 2A (type soundness) and 3 (animation of the semantics).

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.

Enjoy!


Xavier Leroy, 2007-01-11