{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T05:20:26Z","timestamp":1772515226477,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,16]],"date-time":"2018-01-16T00:00:00Z","timestamp":1516060800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DMS-1128155"],"award-info":[{"award-number":["DMS-1128155"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA9550-15-1-0053"],"award-info":[{"award-number":["FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-14-1-0096"],"award-info":[{"award-number":["FA9550-14-1-0096"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["12386"],"award-info":[{"award-number":["12386"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["637339 (CoqHoTT)"],"award-info":[{"award-number":["637339 (CoqHoTT)"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018615","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"164-172","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["The HoTT library: a formalization of homotopy type theory in Coq"],"prefix":"10.1145","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[{"name":"University of Ljubljana, Slovenia"}]},{"given":"Jason","family":"Gross","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Peter LeFanu","family":"Lumsdaine","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden"}]},{"given":"Michael","family":"Shulman","sequence":"additional","affiliation":[{"name":"University of San Diego, USA"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"key":"e_1_3_2_1_2_1","volume-title":"Partiality, revisited: The partiality monad as a quotient inductive-inductive type. Preprint, arXiv:1610.09254","author":"Altenkirch T.","year":"2016","unstructured":"T. Altenkirch, N. A. Danielsson, and N. Kraus. Partiality, revisited: The partiality monad as a quotient inductive-inductive type. Preprint, arXiv:1610.09254, 2016."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_4_1","volume-title":"Private inductive types: Proposing a language extension","author":"Bertot Y.","year":"2013","unstructured":"Y. Bertot. Private inductive types: Proposing a language extension. 2013."},{"key":"e_1_3_2_1_5_1","volume-title":"HoTTSQL: Proving query rewrites with univalent SQL semantics. Preprint, arXiv: 1607.04822","author":"Chu S.","year":"2016","unstructured":"S. Chu, K. Weitz, A. Cheung, and D. Suciu. HoTTSQL: Proving query rewrites with univalent SQL semantics. Preprint, arXiv: 1607.04822, 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. Types for Proofs and Programs (TYPES 2015)","author":"Cohen C.","year":"2016","unstructured":"C. Cohen, T. Coquand, S. Huber, and A. M\u00f6rtberg. Cubical type theory: a constructive interpretation of the univalence axiom. To appear, Proc. Types for Proofs and Programs (TYPES 2015), 2016."},{"key":"e_1_3_2_1_8_1","unstructured":"G. Gonthier A. Mahboubi and E. Tassi. A Small Scale Reflection Extension for the Coq system. Research Report RR-6455 Inria Saclay \u02c6Ile de France 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_18"},{"issue":"1","key":"e_1_3_2_1_10_1","first-page":"1106","article-title":"Type classes for efficient exact real arithmetic","volume":"1","author":"Krebbers R.","year":"2013","unstructured":"R. Krebbers and B. Spitters. Type classes for efficient exact real arithmetic in Coq. LMCS, 9(1:1):1\u201327, 2013. arXiv:1106.3448","journal-title":"Coq. LMCS, 9"},{"key":"e_1_3_2_1_11_1","volume-title":"Modeling set theory in homotopy type theory","author":"Ledent J.","year":"2014","unstructured":"J. Ledent. Modeling set theory in homotopy type theory, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.185.5"},{"key":"e_1_3_2_1_13_1","volume-title":"Modalities in homotopy type theory. In preparation","author":"Rijke E.","year":"2016","unstructured":"E. Rijke, M. Shulman, and B. Spitters. Modalities in homotopy type theory. In preparation, 2016."},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. 9th Workshop on Quantum Physics and Logic, QPL 2012","author":"Schreiber U.","year":"2012","unstructured":"U. Schreiber and M. Shulman. Quantum gauge field theory in cohesive homotopy type theory. In R. Duncan and P. Panangaden, editors, Proc. 9th Workshop on Quantum Physics and Logic, QPL 2012, 2012. arXiv:1408.0054."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_1_16_1","unstructured":"arXiv:1203.3253"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"M. Shulman. Idempotents in intensional type theory. arXiv: 1507.03634; to appear in Logical Methods in Computer Science 2015b. M. Sozeau. Equations: A dependent pattern-matching compiler. In M. Kaufmann and L. C. Paulson editors Proc. Interactive Theorem Proving 2010 volume 6172 of LNCS pages 419\u2013434. Springer 2010a. M. Sozeau. A new look at generalized rewriting in type theory. Journal of Formalized Reasoning 2(1):41\u201362 2010b. M. Sozeau and N. Tabareau. Universe polymorphism in Coq. In G. Klein and R. Gamboa editors Proc. Interactive Theorem Proving 2010 volume 8558 of LNCS pages 499\u2013514. Springer 2014. 10.1007\/978-3-642-14052-5_29","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_36"},{"key":"e_1_3_2_1_20_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"key":"e_1_3_2_1_21_1","unstructured":"V. Voevodsky. A very short note on the homotopy \u03bb-calculus. http:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_ Foundations_files\/Hlambda_short_current.pdf 2006."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"},{"key":"e_1_3_2_1_23_1","volume-title":"UniMath: Univalent Mathematics. https:\/\/github.com\/UniMath","author":"Voevodsky V.","year":"2016","unstructured":"V. Voevodsky, B. Ahrens, D. Grayson, et al. UniMath: Univalent Mathematics. https:\/\/github.com\/UniMath, 2016."}],"event":{"name":"CPP '17: Certified Proofs and Programs","location":"Paris France","acronym":"CPP '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018615","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018615","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018615","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:35:18Z","timestamp":1763458518000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018615"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":23,"alternative-id":["10.1145\/3018610.3018615","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018615","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}