{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T05:20:23Z","timestamp":1772515223294,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,5]],"date-time":"2017-07-05T00:00:00Z","timestamp":1499212800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA-95501210370,FA-95501510053"],"award-info":[{"award-number":["FA-95501210370,FA-95501510053"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006435","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1116703,DMS-1128155,W911-NF0910273,W911-NF1310154"],"award-info":[{"award-number":["CCF-1116703,DMS-1128155,W911-NF0910273,W911-NF1310154"]}],"id":[{"id":"10.13039\/100006435","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005235","name":"Institute for Advanced Study","doi-asserted-by":"publisher","award":["Oswald Veblen"],"award-info":[{"award-number":["Oswald Veblen"]}],"id":[{"id":"10.13039\/100005235","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2934545","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T09:34:47Z","timestamp":1476437687000},"page":"565-574","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory"],"prefix":"10.1145","author":[{"given":"Kuen-Bang","family":"Hou (Favonia)","sequence":"first","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Eric","family":"Finster","sequence":"additional","affiliation":[{"name":"LIX\/\u00c9cole Polytechnique"}]},{"given":"Daniel R.","family":"Licata","sequence":"additional","affiliation":[{"name":"Wesleyan University"}]},{"given":"Peter LeFanu","family":"Lumsdaine","sequence":"additional","affiliation":[{"name":"Stockholm University"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The generalized Blakers-Massey theorem. In preparation","author":"Anel M.","year":"2016","unstructured":"M. Anel, G. Biedermann, E. Finster, and A. Joyal. The generalized Blakers-Massey theorem. In preparation, 2016."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969346"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969428"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969744"},{"key":"e_1_3_2_1_6_1","volume-title":"November","author":"Cavallo E.","year":"2014","unstructured":"E. Cavallo. The Mayer--Vietoris sequence in HoTT. Talk at Oxford Workshop on Homotopy Type Theory, November 2014."},{"key":"e_1_3_2_1_7_1","volume-title":"INRIA","author":"Team Coq Development","year":"2009","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual, version 8.2. INRIA, 2009. Available from http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_8_1","volume-title":"The Blakers-Massey theorem in \u221e-topoi and homotopy type theory. In preparation","author":"Finster E.","year":"2013","unstructured":"E. Finster, D. R. Licata, and P. L. Lumsdaine. The Blakers-Massey theorem in \u221e-topoi and homotopy type theory. In preparation, 2013."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_3_2_1_10_1","volume-title":"Uniform fibrations and the Frobenius condition. arXiv:1510.00669","author":"Gambino N.","year":"2015","unstructured":"N. Gambino and C. Sattler. Uniform fibrations and the Frobenius condition. arXiv:1510.00669, 2015."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_3_2_1_12_1","volume-title":"May","author":"K.-B.","year":"2014","unstructured":"K.-B. Hou (Favonia). Covering spaces in homotopy type theory. Talk at TYPES, May 2014."},{"key":"e_1_3_2_1_13_1","volume-title":"The simplicial model of univalent foundations. arXiv:1211.2851","author":"Kapulkin C.","year":"2012","unstructured":"C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. arXiv:1211.2851, 2012."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"e_1_3_2_1_19_1","unstructured":"P. L. Lumsdaine. Higher inductive types: a tour of the menagerie. http:\/\/homotopytypetheory.org\/2011\/04\/24\/higher-inductive-types-a-tour-of-the-menagerie\/ April 2011."},{"key":"e_1_3_2_1_20_1","volume-title":"Higher inductive types. In preparation","author":"Lumsdaine P. L.","year":"2013","unstructured":"P. L. Lumsdaine and M. Shulman. Higher inductive types. In preparation, 2013."},{"key":"e_1_3_2_1_21_1","volume-title":"A Concise Course in Algebraic Topology","author":"May P.","year":"1999","unstructured":"P. May. A Concise Course in Algebraic Topology. University of Chicago Press, 1999."},{"key":"e_1_3_2_1_22_1","unstructured":"U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis Chalmers University of Technology 2007."},{"key":"e_1_3_2_1_23_1","volume-title":"Toposes and homotopy toposes. Version 0.15","author":"Rezk C.","year":"2010","unstructured":"C. Rezk. Toposes and homotopy toposes. Version 0.15, 2010."},{"key":"e_1_3_2_1_24_1","volume-title":"Available from http:\/\/www.math.uiuc.edu\/~rezk\/freudenthal-and-blakers-massey.pdf","author":"Rezk C.","year":"2015","unstructured":"C. Rezk. Proof of the Blakers-Massey theorem. Available from http:\/\/www.math.uiuc.edu\/~rezk\/freudenthal-and-blakers-massey.pdf, 2015."},{"key":"e_1_3_2_1_25_1","unstructured":"M. Shulman. Homotopy type theory VI: higher inductive types. http:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html April 2011a."},{"key":"e_1_3_2_1_26_1","unstructured":"M. Shulman. A formal proof that π1(S1) = Z. http:\/\/homotopytypetheory.org\/2011\/04\/29\/a-formal-proof-that-pi1s1-is-z\/ April 2011b."},{"key":"e_1_3_2_1_27_1","volume-title":"Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity. arXiv:1203.3253","author":"Shulman M.","year":"2013","unstructured":"M. Shulman. Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity. arXiv:1203.3253, 2013."},{"key":"e_1_3_2_1_28_1","volume-title":"Univalence for inverse EI diagrams. arXiv:1508.02410","author":"Shulman M.","year":"2015","unstructured":"M. Shulman. Univalence for inverse EI diagrams. arXiv:1508.02410, 2015."},{"key":"e_1_3_2_1_29_1","volume-title":"Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book, 2013."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_31_1","unstructured":"V. Voevodsky. A very short note on homotopy \u03bb-calculus. http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf September 2006."},{"key":"e_1_3_2_1_32_1","volume-title":"Carnegie Mellon University","author":"Warren M. A.","year":"2008","unstructured":"M. A. Warren. Homotopy theoretic aspects of constructive type theory. PhD thesis, Carnegie Mellon University, 2008."}],"event":{"name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"New York NY USA","acronym":"LICS '16","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934545","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2934545","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2934545","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:45:39Z","timestamp":1763459139000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934545"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":32,"alternative-id":["10.1145\/2933575.2934545","10.1145\/2933575"],"URL":"https:\/\/doi.org\/10.1145\/2933575.2934545","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}