[POPLmark] A Comparison of Representations

[Arthur Chargueraud]

Dear all,

I am working on a detailed comparison between the several representations
for bindings that have been used in solutions submitted to the challenge so far.

For the time being I am focusing on the properties of subtyping itself
(this corresponds to part 1A, plus lemma A.10 of the challenge). Furthermore,
I restrict my investigations to concrete representations (no higher order),
that is:  named variables, nominal, de Bruijn indices, de Bruijn levels,
locally named, and locally nameless, and their little variations.
(did I forget any important one?)

Please let me know if you can think of any litterature related to such a
comparison.

Thanks!

Arthur Charguéraud