{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:17:15Z","timestamp":1781893035359,"version":"3.54.5"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            Homotopy type theory proposes\n            <jats:italic>higher inductive types<\/jats:italic>\n            (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.\n          <\/jats:p>","DOI":"10.1145\/3290314","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Higher inductive types in cubical computational type theory"],"prefix":"10.1145","volume":"3","author":[{"given":"Evan","family":"Cavallo","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.33"},{"key":"e_1_2_2_3_1","volume-title":"Licata","author":"Angiuli Carlo","year":"2017","unstructured":"Carlo Angiuli , Guillaume Brunerie , Thierry Coquand , Kuen-Bang Hou (Favonia), Robert Harper , and Daniel R . Licata . 2017 a. Cartesian Cubical Type Theory . (Dec. 2017). https:\/\/github.com\/dlicata335\/cart- cube . Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. 2017a. Cartesian Cubical Type Theory. (Dec. 2017). https:\/\/github.com\/dlicata335\/cart- cube ."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"e_1_2_2_5_1","volume-title":"Computational higher type theory III: Univalent universes and exact equality. (Dec","author":"Angiuli Carlo","year":"2017","unstructured":"Carlo Angiuli , Kuen-Bang Hou (Favonia), and Robert Harper . 2017c. Computational higher type theory III: Univalent universes and exact equality. (Dec . 2017 ). arXiv:1712.01800 . Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2017c. Computational higher type theory III: Univalent universes and exact equality. (Dec. 2017). arXiv:1712.01800 ."},{"key":"e_1_2_2_6_1","volume-title":"Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018","author":"Angiuli Carlo","year":"2018","unstructured":"Carlo Angiuli , Kuen-Bang Hou (Favonia), and Robert Harper . 2018 . Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018 , September 4-7, 2018, Birmingham, United Kingdom. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, United Kingdom."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_2_2_8_1","first-page":"63","article-title":"Higher Inductive Types in Programming","volume":"23","author":"Basold Henning","year":"2017","unstructured":"Henning Basold , Herman Geuvers , and Niels van der Weide . 2017 . Higher Inductive Types in Programming . J. UCS 23 , 1 (2017), 63 \u2013 88 . Henning Basold, Herman Geuvers, and Niels van der Weide. 2017. Higher Inductive Types in Programming. J. UCS 23, 1 (2017), 63\u201388.","journal-title":"J. UCS"},{"key":"e_1_2_2_9_1","volume-title":"19th International Conference on Types for Proofs and Programs, TYPES 2013","author":"Bezem Marc","year":"2013","unstructured":"Marc Bezem , Thierry Coquand , and Simon Huber . 2013 . A Model of Type Theory in Cubical Sets . In 19th International Conference on Types for Proofs and Programs, TYPES 2013 , April 22-26, 2013, Toulouse, France. 107\u2013128. Marc Bezem, Thierry Coquand, and Simon Huber. 2013. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France. 107\u2013128."},{"key":"e_1_2_2_10_1","volume-title":"Computational higher type theory IV: Inductive types. (Jan","author":"Cavallo Evan","year":"2018","unstructured":"Evan Cavallo and Robert Harper . 2018. Computational higher type theory IV: Inductive types. (Jan . 2018 ). arXiv:1801.01568 . Evan Cavallo and Robert Harper. 2018. Computational higher type theory IV: Inductive types. (Jan. 2018). arXiv:1801.01568 ."},{"key":"e_1_2_2_11_1","volume-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015","author":"Cohen Cyril","year":"2015","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2015 . Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015 , May 18-21, 2015, Tallinn, Estonia. 5:1\u20135:34. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2015. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia. 5:1\u20135:34."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_13_1","volume-title":"International Conference on Computer Logic, Tallinn, USSR","author":"Coquand Thierry","year":"1988","unstructured":"Thierry Coquand and Christine Paulin . 1988 . Inductively defined types. In COLOG-88 , International Conference on Computer Logic, Tallinn, USSR , December 1988, Proceedings. 50\u201366. Thierry Coquand and Christine Paulin. 1988. Inductively defined types. In COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings. 50\u201366."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_2_2_15_1","volume-title":"33rd International Conference","author":"Dybjer Peter","year":"2017","unstructured":"Peter Dybjer and Hugo Moeneclaey . 2017 . Finitary Higher Inductive Types in the Groupoid Model. In Mathematical Foundations of Programming Semantics , 33rd International Conference , Ljubljana, Slovenia. Peter Dybjer and Hugo Moeneclaey. 2017. Finitary Higher Inductive Types in the Groupoid Model. In Mathematical Foundations of Programming Semantics, 33rd International Conference, Ljubljana, Slovenia."},{"key":"e_1_2_2_16_1","volume-title":"Twenty-five years of constructive type theory (Venice","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann and Thomas Streicher . 1998. The groupoid interpretation of type theory . In Twenty-five years of constructive type theory (Venice , 1995 ). Oxford Logic Guides, Vol . 36. Oxford Univ. Press , New York, 83\u2013111. Martin Hofmann and Thomas Streicher. 1998. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995). Oxford Logic Guides, Vol. 36. Oxford Univ. Press, New York, 83\u2013111."},{"key":"e_1_2_2_18_1","volume-title":"3nd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","author":"Kaposi Ambrus","year":"2018","unstructured":"Ambrus Kaposi and Andr\u00e1s Kov\u00e1cs . 2018 . A syntax for higher inductive-inductive types . In 3nd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 , July 9-12, 2018, Oxford, UK. Ambrus Kaposi and Andr\u00e1s Kov\u00e1cs. 2018. A syntax for higher inductive-inductive types. In 3nd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933586"},{"key":"e_1_2_2_20_1","unstructured":"Peter LeFanu Lumsdaine. 2011. Model Structures from Higher Inductive Types. (2011). Unpublished note. http: \/\/peterlefanulumsdaine.com\/research\/Lumsdaine- Model- strux- from- HITs.pdf .  Peter LeFanu Lumsdaine. 2011. Model Structures from Higher Inductive Types. (2011). Unpublished note. http: \/\/peterlefanulumsdaine.com\/research\/Lumsdaine- Model- strux- from- HITs.pdf ."},{"key":"e_1_2_2_21_1","volume-title":"Semantics of higher inductive types. (May","author":"LeFanu Lumsdaine Peter","year":"2017","unstructured":"Peter LeFanu Lumsdaine and Michael Shulman . 2017. Semantics of higher inductive types. (May 2017 ). arXiv:1705.07088 . Peter LeFanu Lumsdaine and Michael Shulman. 2017. Semantics of higher inductive types. (May 2017). arXiv:1705.07088 ."},{"key":"e_1_2_2_22_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"80","author":"Martin-L\u00f6f Per","year":"1975","unstructured":"Per Martin-L\u00f6f . 1975 . An intuitionistic theory of types: predicative part. In Logic Colloquium \u201973, H.E. Rose and J.C. Shepherdson (Eds.) . Studies in Logic and the Foundations of Mathematics , Vol. 80 . North-Holland, 73\u2013118. Per Martin-L\u00f6f. 1975. An intuitionistic theory of types: predicative part. In Logic Colloquium \u201973, H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. North-Holland, 73\u2013118."},{"key":"e_1_2_2_23_1","volume-title":"Podewski (Eds.)","author":"Martin-L\u00f6f Per","year":"1982","unstructured":"Per Martin-L\u00f6f . 1982 . Constructive Mathematics and Computer Programming. In Logic, Methodology and Philosophy of Science, L.J. Cohen, J. \u0141o\u015b, H. Pfeiffer, and K.-P . Podewski (Eds.) , Vol. VI . 153\u2013175. Per Martin-L\u00f6f. 1982. Constructive Mathematics and Computer Programming. In Logic, Methodology and Philosophy of Science, L.J. Cohen, J. \u0141o\u015b, H. Pfeiffer, and K.-P. Podewski (Eds.), Vol. VI. 153\u2013175."},{"key":"e_1_2_2_24_1","volume-title":"The join construction. (Jan","author":"Rijke Egbert","year":"2017","unstructured":"Egbert Rijke . 2017. The join construction. (Jan . 2017 ). arXiv:1701.07538 . Egbert Rijke. 2017. The join construction. (Jan. 2017). arXiv:1701.07538 ."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_2_2_26_1","volume-title":"An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. (Sept","author":"Swan Andrew","year":"2014","unstructured":"Andrew Swan . 2014. An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. (Sept . 2014 ). arXiv:1409.1829 . Andrew Swan. 2014. An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. (Sept. 2014). arXiv:1409.1829 ."},{"key":"e_1_2_2_27_1","volume-title":"Identity Types in Algebraic Model Structures and Cubical Sets. (Aug","author":"Swan Andrew","year":"2018","unstructured":"Andrew Swan . 2018a. Identity Types in Algebraic Model Structures and Cubical Sets. (Aug . 2018 ). arXiv:1808.00915 . Andrew Swan. 2018a. Identity Types in Algebraic Model Structures and Cubical Sets. (Aug. 2018). arXiv:1808.00915 ."},{"key":"e_1_2_2_28_1","volume-title":"Separating Path and Identity Types in Presheaf Models of Univalent Type Theory. (Aug","author":"Swan Andrew","year":"2018","unstructured":"Andrew Swan . 2018b. Separating Path and Identity Types in Presheaf Models of Univalent Type Theory. (Aug . 2018 ). arXiv:1808.00920 . Andrew Swan. 2018b. Separating Path and Identity Types in Presheaf Models of Univalent Type Theory. (Aug. 2018). arXiv:1808.00920 ."},{"key":"e_1_2_2_29_1","unstructured":"The RedPRL Development Team. 2018a. RedPRL \u2013 the People\u2019s Refinement Logic. (2018). http:\/\/www.redprl.org\/  The RedPRL Development Team. 2018a. RedPRL \u2013 the People\u2019s Refinement Logic. (2018). http:\/\/www.redprl.org\/"},{"key":"e_1_2_2_30_1","unstructured":"The RedPRL Development Team. 2018b. redtt. (2018). https:\/\/github.com\/RedPRL\/redtt  The RedPRL Development Team. 2018b. redtt. (2018). https:\/\/github.com\/RedPRL\/redtt"},{"key":"e_1_2_2_31_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book , Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book , Institute for Advanced Study."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854076"},{"key":"e_1_2_2_33_1","unstructured":"Vladimir Voevodsky. 2010. The equivalence axiom and univalent models of type theory. (2010). http:\/\/www.math.ias.edu\/ vladimir\/files\/CMU_talk.pdf Notes from a talk at Carnegie Mellon University.  Vladimir Voevodsky. 2010. The equivalence axiom and univalent models of type theory. (2010). http:\/\/www.math.ias.edu\/ vladimir\/files\/CMU_talk.pdf Notes from a talk at Carnegie Mellon University."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290314","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290314","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290314","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290314"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290314"],"URL":"https:\/\/doi.org\/10.1145\/3290314","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}