Gaëtan Gilbert. Formalising real numbers in homotopy type theory. 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 112-124, ACM, 2017. [doi]
@inproceedings{Gilbert17,
title = {Formalising real numbers in homotopy type theory},
author = {Gaëtan Gilbert},
year = {2017},
doi = {10.1145/3018610.3018614},
url = {http://doi.acm.org/10.1145/3018610.3018614},
researchr = {https://researchr.org/publication/Gilbert17},
cites = {0},
citedby = {0},
pages = {112-124},
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},
}