# Publication details

##
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)

@INPROCEEDINGS{KaiserEtAl:2017:sysf_pts_equiv_coq,
title = {Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas},
author = {Jonas Kaiser and Tobias Tebbi and Gert Smolka},
year = {2017},
month = {Jan},
booktitle = {Proceedings of CPP 2017},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009