@Article{bauer_et_al:DagRep.8.8.130, author = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, title = {{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}}, pages = {130--145}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2019}, volume = {8}, number = {8}, editor = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.8.130}, URN = {urn:nbn:de:0030-drops-102370}, doi = {10.4230/DagRep.8.8.130}, annote = {Keywords: formal methods, formalized mathematics, proof assistant, type theory} }