{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:52Z","timestamp":1772164072198,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,14]]},"DOI":"10.1145\/2676726.2676983","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"31-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Higher Inductive Types as Homotopy-Initial Algebras"],"prefix":"10.1145","author":[{"given":"Kristina","family":"Sojakova","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, PITTSBURGH, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_3_2_2_4_1","volume-title":"A model of type theory in cubical sets","author":"Bezem M.","year":"2014","unstructured":"M. Bezem , T. Coquand , and S. Huber . A model of type theory in cubical sets , 2014 . Available at http:\/\/www.cse.chalmers.se\/~coquand\/mod1.pdf. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets, 2014. Available at http:\/\/www.cse.chalmers.se\/~coquand\/mod1.pdf."},{"key":"e_1_3_2_2_5_1","volume-title":"INRIA","author":"Team Coq Development","year":"2012","unstructured":"Coq Development Team . The Coq Proof Assistant Reference Manual, version 8.4pl3 . INRIA , 2012 . Available at coq.inria.fr. Coq Development Team. The Coq Proof Assistant Reference Manual, version 8.4pl3. INRIA, 2012. Available at coq.inria.fr."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_3_2_2_8_1","series-title":"Oxford Logic Guides","first-page":"83","volume-title":"Twenty-five years of constructive type theory","author":"Hofmann M.","year":"1995","unstructured":"M. Hofmann and T. Streicher . The groupoid interpretation of type theory . In Twenty-five years of constructive type theory 1995 , volume 36 of Oxford Logic Guides , pages 83 -- 111 . Oxford Univ. Press , 1998. M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory 1995, volume 36 of Oxford Logic Guides, pages 83--111. Oxford Univ. Press, 1998."},{"key":"e_1_3_2_2_9_1","volume-title":"The simplicial model of univalent foundations. Available as arXiv:1211.2851v1","author":"Kapulkin C.","year":"2012","unstructured":"C. Kapulkin , P. Lumsdaine , and V. Voevodsky . The simplicial model of univalent foundations. Available as arXiv:1211.2851v1 , 2012 . C. Kapulkin, P. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. Available as arXiv:1211.2851v1, 2012."},{"key":"e_1_3_2_2_10_1","volume-title":"The truncation map |_| : N -- ||N|| is nearly invertible","author":"Kraus N.","year":"2013","unstructured":"N. Kraus . The truncation map |_| : N -- ||N|| is nearly invertible , 2013 . Post on the Homotopy Type Theory blog. N. Kraus. The truncation map |_| : N -- ||N|| is nearly invertible, 2013. Post on the Homotopy Type Theory blog."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:24)2010"},{"key":"e_1_3_2_2_15_1","volume-title":"Higher inductive types: a tour of the menagerie","author":"Lumsdaine P.","year":"2011","unstructured":"P. Lumsdaine . Higher inductive types: a tour of the menagerie , 2011 . Post on the Homotopy Type Theory blog. P. Lumsdaine. Higher inductive types: a tour of the menagerie, 2011. Post on the Homotopy Type Theory blog."},{"key":"e_1_3_2_2_16_1","volume-title":"Semantics of higher inductive types","author":"Lumsdaine P.","year":"2012","unstructured":"P. Lumsdaine and M. Shulman . Semantics of higher inductive types , 2012 . Available at http:\/\/uf-ias-2012.wikispaces.com\/file\/view\/semantics.pdf. P. Lumsdaine and M. Shulman. Semantics of higher inductive types, 2012. Available at http:\/\/uf-ias-2012.wikispaces.com\/file\/view\/semantics.pdf."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_2_20_1","volume-title":"VI","author":"Shulman M.","year":"2011","unstructured":"M. Shulman . Homotopy Type Theory , VI , 2011 . Post on the n- category cafe blog. M. Shulman. Homotopy Type Theory, VI, 2011. Post on the n- category cafe blog."},{"key":"e_1_3_2_2_21_1","volume-title":"Higher inductive types as homotopy-initial algebras","author":"Sojakova K.","year":"2014","unstructured":"K. Sojakova . Higher inductive types as homotopy-initial algebras . Technical Report Carnegie Mellon University-CS-14--101R, Carnegie Mellon University , 2014 . Available at http:\/\/reports-archive.adm.cs.cmu.edu\/. K. Sojakova. Higher inductive types as homotopy-initial algebras. Technical Report Carnegie Mellon University-CS-14--101R, Carnegie Mellon University, 2014. Available at http:\/\/reports-archive.adm.cs.cmu.edu\/."},{"key":"e_1_3_2_2_22_1","volume-title":"Investigations into intensional type theory. Habilitation Thesis. Available from the authors web page","author":"Streicher T.","year":"1993","unstructured":"T. Streicher . Investigations into intensional type theory. Habilitation Thesis. Available from the authors web page , 1993 . T. Streicher. Investigations into intensional type theory. Habilitation Thesis. Available from the authors web page, 1993."},{"key":"e_1_3_2_2_23_1","volume-title":"Univalent Foundations Project","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program , Institute for Advanced Study. Homotopy Type Theory - Univalent Foundations of Mathematics . Univalent Foundations Project , 2013 . The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory - Univalent Foundations of Mathematics. Univalent Foundations Project, 2013."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071371"},{"key":"e_1_3_2_2_26_1","volume-title":"Language, Information and Computation (WoLLIC","author":"Voevodsky V.","year":"2011","unstructured":"V. Voevodsky . Univalent foundations of mathematics, 2011. Invited talk at the Workshop on Logic , Language, Information and Computation (WoLLIC 2011 ). V. Voevodsky. Univalent foundations of mathematics, 2011. Invited talk at the Workshop on Logic, Language, Information and Computation (WoLLIC 2011)."}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676983","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2676983","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:03Z","timestamp":1750212783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676983"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":25,"alternative-id":["10.1145\/2676726.2676983","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2676983","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2676983","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}