{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:38:03Z","timestamp":1767926283483,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,7,14]],"date-time":"2014-07-14T00:00:00Z","timestamp":1405296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000121","name":"Division of Mathematical Sciences","doi-asserted-by":"publisher","award":["DMS-1128155"],"award-info":[{"award-number":["DMS-1128155"]}],"id":[{"id":"10.13039\/100000121","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005235","name":"Institute for Advanced Study","doi-asserted-by":"publisher","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":[[2014,7,14]]},"DOI":"10.1145\/2603088.2603153","type":"proceedings-article","created":{"date-parts":[[2014,7,28]],"date-time":"2014-07-28T13:21:45Z","timestamp":1406553705000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Eilenberg-MacLane spaces in homotopy type theory"],"prefix":"10.1145","author":[{"given":"Daniel R.","family":"Licata","sequence":"first","affiliation":[{"name":"Wesleyan University"}]},{"given":"Eric","family":"Finster","sequence":"additional","affiliation":[{"name":"Inria Paris Rocquencourt"}]}],"member":"320","published-online":{"date-parts":[[2014,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ill.","author":"Adams J. F.","year":"1974"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_3_1","unstructured":"B. Barras T. Coquand and S. Huber. A generalization of Takeuti-Gandy interpretations. To appear in Mathematical Structures in Computer Science 2013.  B. Barras T. Coquand and S. Huber. A generalization of Takeuti-Gandy interpretations. To appear in Mathematical Structures in Computer Science 2013."},{"key":"e_1_3_2_1_4_1","volume-title":"Preprint","author":"Bezem M.","year":"2013"},{"key":"e_1_3_2_1_5_1","unstructured":"G. Brunerie. Truncations and truncated higher inductive types. http:\/\/homotopytypetheory.org\/2012\/09\/16\/truncations-and-truncated-higher-inductive-types\/ 2012.  G. Brunerie. Truncations and truncated higher inductive types. http:\/\/homotopytypetheory.org\/2012\/09\/16\/truncations-and-truncated-higher-inductive-types\/ 2012."},{"key":"e_1_3_2_1_6_1","volume-title":"INRIA","author":"Team Coq Development","year":"2009"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_3_2_1_9_1","volume-title":"Twenty-five years of constructive type theory","author":"Hofmann M.","year":"1998"},{"key":"e_1_3_2_1_10_1","unstructured":"C. Kapulkin P. L. Lumsdaine and V. Voevodsky. The simplicial model of univalent foundations. arXiv:1211.2851 2012.  C. Kapulkin P. L. Lumsdaine and V. Voevodsky. The simplicial model of univalent foundations. arXiv:1211.2851 2012."},{"key":"e_1_3_2_1_11_1","unstructured":"D. R. Licata. Running circles around (in) your proof assistant; or quotients that compute. http:\/\/homotopytypetheory.org\/2011\/04\/23\/running-circles-around-in-your-proof-assistant\/ April 2011.  D. R. Licata. Running circles around (in) your proof assistant; or quotients that compute. http:\/\/homotopytypetheory.org\/2011\/04\/23\/running-circles-around-in-your-proof-assistant\/ April 2011."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"e_1_3_2_1_16_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.  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_17_1","unstructured":"P. L. Lumsdaine and M. Shulman. Higher inductive types. In preparation 2013.  P. L. Lumsdaine and M. Shulman. Higher inductive types. In preparation 2013."},{"key":"e_1_3_2_1_18_1","volume-title":"Chalmers University of Technology","author":"Norell U.","year":"2007"},{"key":"e_1_3_2_1_19_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 2011.  M. Shulman. Homotopy type theory VI: higher inductive types. http:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html April 2011."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"M. Shulman. Univalence for inverse diagrams and homotopy canonicity. To appear in Mathematical Structures in Computer Science; arXiv:1203.3253 2013.  M. Shulman. Univalence for inverse diagrams and homotopy canonicity. To appear in Mathematical Structures in Computer Science ; arXiv:1203.3253 2013.","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_1_21_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_23_1","volume-title":"Information and Computation","author":"Voevodsky V.","year":"2011"},{"key":"e_1_3_2_1_24_1","volume-title":"Carnegie Mellon University","author":"Warren M. A.","year":"2008"},{"key":"e_1_3_2_1_25_1","unstructured":"G. W.\n       \n      Whitehead\n    .\n      \n  \n   \n  Elements of homotopy theory volume \n  61\n   of \n  Graduate Texts in Mathematics\n  . \n  Springer-Verlag New York 1978\n  . ISBN 0-387-90336-4.  G. W. Whitehead. Elements of homotopy theory volume 61 of Graduate Texts in Mathematics . Springer-Verlag New York 1978. ISBN 0-387-90336-4."}],"event":{"name":"CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC","location":"Vienna Austria","acronym":"CSL-LICS '14","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2603088.2603153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2603088.2603153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:41Z","timestamp":1750230101000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2603088.2603153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,14]]},"references-count":25,"alternative-id":["10.1145\/2603088.2603153","10.1145\/2603088"],"URL":"https:\/\/doi.org\/10.1145\/2603088.2603153","relation":{},"subject":[],"published":{"date-parts":[[2014,7,14]]},"assertion":[{"value":"2014-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}