Jonas Kaiser, Tobias Tebbi, Gert Smolka. Equivalence of system f and ź2 in Coq based on context morphism lemmas. In Yves Bertot, Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pages 222-234, ACM, 2017. [doi]
@inproceedings{KaiserTS17,
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},
doi = {10.1145/3018610.3018618},
url = {http://doi.acm.org/10.1145/3018610.3018618},
researchr = {https://researchr.org/publication/KaiserTS17},
cites = {0},
citedby = {0},
pages = {222-234},
booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017},
editor = {Yves Bertot and Viktor Vafeiadis},
publisher = {ACM},
isbn = {978-1-4503-4705-1},
}