Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq formal proof of the LaxMilgram theorem. 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 79-89, ACM, 2017. [doi]
Abstract is missing.