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.
<a href="https://www.ps.uni-saarland.de/extras/cpp17-sysf/index.php">Further Material (e.g. Coq sources)</a>
Download PDF Show BibTeX Download slides (PDF)