Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters. The HoTT library: a formalization of homotopy type theory in Coq. 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 164-172, ACM, 2017. [doi]
@inproceedings{BauerGLSSS17,
title = {The HoTT library: a formalization of homotopy type theory in Coq},
author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters},
year = {2017},
doi = {10.1145/3018610.3018615},
url = {http://doi.acm.org/10.1145/3018610.3018615},
researchr = {https://researchr.org/publication/BauerGLSSS17},
cites = {0},
citedby = {0},
pages = {164-172},
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},
}