We give a machine-checked proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system variant λ2. This is established by reducing the typing problem of F to λ2 and vice versa. The difficulty lies in aligning different binding-structures and different contexts (dependent vs. non-dependent). The use of de Bruijn syntax, parallel substitutions, and context morphism lemmas leads to an elegant proof. We use the Coq proof assistant and the substitution library Autosubst.
This work is going to appear at the CPP 2017 conference in Paris, France. A preliminary version of this work was presented at the HOR 2016 workshop in Porto, Portugal. An extended abstract and the workshop presentation slides are linked below.
We have conducted a second proof using HOAS and syntax relations, formalised in Abella. The results were presented at the TTT 2017 workshop, also in Paris. The respective project details can be found here.