{"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":1772515223298,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0053"],"award-info":[{"award-number":["FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009861","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"680-693","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Computational higher-dimensional type theory"],"prefix":"10.1145","author":[{"given":"Carlo","family":"Angiuli","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Todd","family":"Wilson","sequence":"additional","affiliation":[{"name":"California State University at Fresno, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/913680"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"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","volume-title":"Preprint","author":"Angiuli C.","year":"2016","unstructured":"C. Angiuli and R. Harper. Computational higher type theory II: Dependent cubical realizability. Preprint, June 2016."},{"key":"e_1_3_2_1_5_1","volume-title":"Preprint","author":"Angiuli C.","year":"2016","unstructured":"C. Angiuli, R. Harper, and T. Wilson. Computational higher type theory I: Abstract cubical realizability. Preprint, April 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628158"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_8_1","first-page":"128","volume-title":"19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs)","author":"Bezem M.","year":"2014","unstructured":"M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107\u2013128, Dagstuhl, Germany, 2014. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_9_1","volume-title":"Preprint","author":"Birkedal L.","year":"2016","unstructured":"L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory: Path equality for guarded recursion. Preprint, June 2016."},{"key":"e_1_3_2_1_10_1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES 2015), Leibniz International Proceedings in Informatics (LIPIcs)","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. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2016. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. To appear."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/4030.4032"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747618"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90085-8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/10510"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.04.010"},{"key":"e_1_3_2_1_17_1","volume-title":"Preprint","author":"Gambino N.","year":"2015","unstructured":"N. Gambino and C. Sattler. Uniform fibrations and the Frobenius condition. Preprint, Oct 2015."},{"issue":"4","key":"e_1_3_2_1_18_1","first-page":"397","article-title":"Natural weak factorization systems","volume":"042","author":"Grandis M.","year":"2006","unstructured":"M. Grandis and W. Tholen. Natural weak factorization systems. Archivum Mathematicum, 042(4):397\u2013408, 2006.","journal-title":"Archivum Mathematicum"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90026-Z"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/3002812"},{"key":"e_1_3_2_1_21_1","volume-title":"Preprint","author":"Harper R.","year":"2015","unstructured":"R. Harper and K.-B. (Favonia) Hou. A note on the uniform Kan condition in nominal cubical sets. Preprint, Jan 2015."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_3_2_1_23_1","unstructured":"S. Huber. Cubical Interpretations of Type Theory. PhD thesis University of Gothenburg Expected November 2016."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.41.12.1092"},{"key":"e_1_3_2_1_25_1","volume-title":"November","author":"Licata D. R.","year":"2014","unstructured":"D. R. Licata and G. Brunerie. A cubical type theory, November 2014."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.19"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70727-4"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1984.0073"},{"key":"e_1_3_2_1_29_1","series-title":"Studies in Proof Theory","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"P. Martin-L\u00f6f. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. ISBN 88-7088-105-9. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"e_1_3_2_1_30_1","series-title":"Logic","first-page":"14","volume-title":"Judgement and the Epistemic Foundation of Logic","author":"Martin-L\u00f6f P.","unstructured":"P. Martin-L\u00f6f. Verificationism then and now. In M. van der Schaar, editor, Judgement and the Epistemic Foundation of Logic, volume 31 of Logic, Epistemology, and the Unity of Science, pages 3\u201314. Springer, 2013. ISBN 978-94-007-5136-1."},{"key":"e_1_3_2_1_31_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_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2512979"},{"key":"e_1_3_2_1_33_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"220","volume-title":"20th International Conference on Types for Proofs and Programs (TYPES","author":"Pitts A. M.","year":"2014","unstructured":"A. M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 202\u2013220, Dagstuhl, Germany, 2015. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. ISBN 978-3-939897- 88-0."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854077"},{"key":"e_1_3_2_1_35_1","volume-title":"Sept 14, 2015.","author":"Rahli V.","unstructured":"V. Rahli and M. Bickford. Coq as a Metatheory for Nuprl with Bar Induction. Presented at Continuity, Computability, Constructivity \u2013 From Logic to Algorithms (CCC 2015), Sept 14, 2015."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/524279"},{"key":"e_1_3_2_1_37_1","unstructured":"J. Sterling D. Gratzer V. Rahli D. Morrison E. Akentyev and A. Tosun. RedPRL \u2013 the People\u2019s Refinement Logic. http:\/\/www. redprl.org\/ 2016."},{"key":"e_1_3_2_1_38_1","volume-title":"The Coq proof assistant","author":"Project The Coq","year":"2016","unstructured":"The Coq Project. The Coq proof assistant, 2016."},{"key":"e_1_3_2_1_39_1","volume-title":"Prl project","author":"Project The","year":"2016","unstructured":"The NuPRL Project. Prl project, 2016."},{"key":"e_1_3_2_1_40_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory. org\/book, Institute for Advanced Study, 2013."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_42_1","volume-title":"A very short note on homotopy \u03bb-calculus, 09","author":"Voevodsky V.","year":"2006","unstructured":"V. Voevodsky. A very short note on homotopy \u03bb-calculus, 09 2006."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/2008862.2008867"},{"key":"e_1_3_2_1_44_1","volume-title":"Feb.","author":"Voevodsky V.","year":"2013","unstructured":"V. Voevodsky. A simple type system with two identity types. Lecture notes, Feb. 2013."},{"key":"e_1_3_2_1_45_1","volume-title":"The UniMath project","author":"Voevodsky V.","year":"2016","unstructured":"V. Voevodsky. The UniMath project, 2016."},{"key":"e_1_3_2_1_46_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."},{"key":"e_1_3_2_1_47_1","volume-title":"Oct","author":"Williamson R.","year":"2012","unstructured":"R. Williamson. Combinatorial homotopy theory. Lecture notes, Oct 2012."}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009861","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009861","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009861","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:43:17Z","timestamp":1763458997000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009861"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":47,"alternative-id":["10.1145\/3009837.3009861","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009861","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009861","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}