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 typability problem of F to λ2 and vice versa. The systems are formulated using higher-order abstract syntax and the proof is executed in the Abella proof system. We compare and contrast this proof to our earlier Coq formalisation based on de Bruijn indices and context morphism lemmas.
This work builds upon prior work that will appear at the CPP 2017 conference in Paris, France. The corresponding project page can be found here.