{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:40Z","timestamp":1772164000705,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,8,19]],"date-time":"2014-08-19T00:00:00Z","timestamp":1408406400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-1116703"],"award-info":[{"award-number":["CCF-1116703"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,8,19]]},"DOI":"10.1145\/2628136.2628158","type":"proceedings-article","created":{"date-parts":[[2014,8,21]],"date-time":"2014-08-21T08:19:23Z","timestamp":1408609163000},"page":"243-256","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Homotopical patch theory"],"prefix":"10.1145","author":[{"given":"Carlo","family":"Angiuli","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edward","family":"Morehouse","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel R.","family":"Licata","sequence":"additional","affiliation":[{"name":"Wesleyan University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,8,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_2_1_2_1","volume-title":"Lyon","author":"Altenkirch T.","year":"2014","unstructured":"T. Altenkirch . Containers in homotopy type theory. Talk at Mathematical Structures of Computation , Lyon , 2014 . T. Altenkirch. Containers in homotopy type theory. Talk at Mathematical Structures of Computation, Lyon, 2014."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_5_1","volume-title":"A generalization of Takeuti-Gandy interpretation. To appear in Mathematical Structures in Computer Science","author":"Barras B.","year":"2013","unstructured":"B. Barras , T. Coquand , and S. Huber . A generalization of Takeuti-Gandy interpretation. To appear in Mathematical Structures in Computer Science , 2013 . B. Barras, T. Coquand, and S. Huber. A generalization of Takeuti-Gandy interpretation. To appear in Mathematical Structures in Computer Science, 2013."},{"key":"e_1_3_2_1_6_1","volume-title":"Preprint","author":"Bezem M.","year":"2013","unstructured":"M. Bezem , T. Coquand , and S. Huber . A model of type theory in cubical sets . Preprint , September 2013 . M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. Preprint, September 2013."},{"key":"e_1_3_2_1_7_1","volume-title":"http:\/\/projects.haskell.org\/camp\/","author":"Project Camp","year":"2010","unstructured":"Camp Project . http:\/\/projects.haskell.org\/camp\/ , 2010 . Camp Project. http:\/\/projects.haskell.org\/camp\/, 2010."},{"key":"e_1_3_2_1_8_1","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , and S. F. Smith . Implementing Mathematics with the NuPRL Proof Development System . Prentice Hall , 1986 . R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986."},{"key":"e_1_3_2_1_9_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\/. 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_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_3_2_1_12_1","volume-title":"Some properties of darcs patch theory. Available from http:\/\/urchin.earth.li\/darcs\/ganesh\/darcs-patch-theory\/theory\/formal.pdf","author":"Ganesh Sittampalam","year":"2005","unstructured":"Ganesh Sittampalam et al. Some properties of darcs patch theory. Available from http:\/\/urchin.earth.li\/darcs\/ganesh\/darcs-patch-theory\/theory\/formal.pdf , 2005 . Ganesh Sittampalam et al. Some properties of darcs patch theory. Available from http:\/\/urchin.earth.li\/darcs\/ganesh\/darcs-patch-theory\/theory\/formal.pdf, 2005."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_3_2_1_14_1","volume-title":"Twenty-five years of constructive type theory","author":"Hofmann M.","year":"1998","unstructured":"M. Hofmann and T. Streicher . The groupoid interpretation of type theory . In Twenty-five years of constructive type theory . Oxford University Press , 1998 . M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory. Oxford University Press, 1998."},{"key":"e_1_3_2_1_15_1","unstructured":"R. Houston. On editing text. http:\/\/bosker.wordpress.com\/2012\/05\/10\/on-editing-text\/ 2012.  R. Houston. On editing text. http:\/\/bosker.wordpress.com\/2012\/05\/10\/on-editing-text\/ 2012."},{"key":"e_1_3_2_1_16_1","volume-title":"A formalization of darcs patch theory using inverse semigroups. Available from ftp:\/\/ftp.math.ucla.edu\/pub\/camreport\/cam09-83.pdf","author":"Jacobson J.","year":"2009","unstructured":"J. Jacobson . A formalization of darcs patch theory using inverse semigroups. Available from ftp:\/\/ftp.math.ucla.edu\/pub\/camreport\/cam09-83.pdf , 2009 . J. Jacobson. A formalization of darcs patch theory using inverse semigroups. Available from ftp:\/\/ftp.math.ucla.edu\/pub\/camreport\/cam09-83.pdf, 2009."},{"key":"e_1_3_2_1_17_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 . C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. arXiv:1211.2851, 2012."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"e_1_3_2_1_25_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_26_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 . P. L. Lumsdaine and M. Shulman. Higher inductive types. In preparation, 2013."},{"key":"e_1_3_2_1_27_1","volume-title":"University of Edinburgh","author":"McBride C.","year":"2000","unstructured":"C. McBride . Dependently Typed Functional Programs and Their Proofs. PhD thesis , University of Edinburgh , 2000 . C. McBride. Dependently Typed Functional Programs and Their Proofs. PhD thesis, University of Edinburgh, 2000."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.018"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088349"},{"key":"e_1_3_2_1_32_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_33_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 . M. Shulman. Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity. arXiv:1203.3253, 2013."},{"key":"e_1_3_2_1_34_1","volume-title":"The semantics of version control. Available from http:\/\/www.staff.science.uu.nl\/~swier004\/","author":"Swierstra W.","year":"2014","unstructured":"W. Swierstra and A. L\u00f6h . The semantics of version control. Available from http:\/\/www.staff.science.uu.nl\/~swier004\/ , 2014 . W. Swierstra and A. L\u00f6h. The semantics of version control. Available from http:\/\/www.staff.science.uu.nl\/~swier004\/, 2014."},{"key":"e_1_3_2_1_35_1","volume-title":"Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program , Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book , 2013 . The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book, 2013."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_37_1","volume-title":"Information and Computation","author":"Voevodsky V.","year":"2011","unstructured":"V. Voevodsky . Univalent foundations of mathematics. Invited talk at WoLLIC 2011 18th Workshop on Logic, Language , Information and Computation , 2011 . V. Voevodsky. Univalent foundations of mathematics. Invited talk at WoLLIC 2011 18th Workshop on Logic, Language, Information and Computation, 2011."}],"event":{"name":"ICFP'14: ACM SIGPLAN International Conference on Functional Programming","location":"Gothenburg Sweden","acronym":"ICFP'14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 19th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2628136.2628158","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2628136.2628158","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:19:38Z","timestamp":1750216778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2628136.2628158"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,19]]},"references-count":34,"alternative-id":["10.1145\/2628136.2628158","10.1145\/2628136"],"URL":"https:\/\/doi.org\/10.1145\/2628136.2628158","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2692915.2628158","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,8,19]]},"assertion":[{"value":"2014-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}