Publication details

Saarland University Computer Science

Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas

Jonas Kaiser, Tobias Tebbi, Gert Smolka

Proceedings of CPP 2017, January 2017

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.

Further Material (e.g. Coq sources)

Download PDF        Show BibTeX        Download slides (PDF)       

Login to edit

Legal notice, Privacy policy