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.
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).