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,
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:
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).
Xavier Leroy, 2007-01-11