Publication details

Saarland University Computer Science

Equivalence of System F and λ2 in Abella

Jonas Kaiser, Gert Smolka

Workshop Presentation at TTT 2017, Paris, 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 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.

Further details, including Abella sources on project page.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009