{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:40Z","timestamp":1767929560079,"version":"3.49.0"},"reference-count":66,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470719","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T16:14:07Z","timestamp":1625674447000},"page":"1-15","source":"Crossref","is-referenced-by-count":18,"title":["Normalization for Cubical Type Theory"],"prefix":"10.1109","author":[{"given":"Jonathan","family":"Sterling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo","family":"Angiuli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511550812"},{"key":"ref38","article-title":"Homotopy canonicity of homotopy type theory","author":"kapulkin","year":"0"},{"key":"ref33","article-title":"Lifting Grothendieck universes","author":"hofmann","year":"1997"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"ref37","article-title":"Gluing for type theory","volume":"131","author":"kaposi","year":"2019","journal-title":"4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037110"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084217"},{"key":"ref34","article-title":"Canonicity for cubical type theory","author":"huber","year":"2018","journal-title":"Journal of Automated Reasoning"},{"key":"ref60","author":"taylor","year":"1999","journal-title":"Practical Foundations of Mathematics"},{"key":"ref62","article-title":"A general framework for the semantics of type theory","author":"uemura","year":"2019"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005084"},{"key":"ref28","article-title":"Syntactic categories for dependent type theory: sketching and adequacy","author":"gratzer","year":"2020"},{"key":"ref63","year":"2013","journal-title":"Homotopy Type Theory Univalent Foundations of Mathematics"},{"key":"ref27","article-title":"On proving that 1 is an indecomposable projective in various free categories","author":"freyd","year":"1978"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"ref65","first-page":"429","author":"vickers","year":"2007","journal-title":"Locales and Toposes as Spaces"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(87)90077-6"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"ref1","article-title":"Normalization by evaluation: Dependent types and impredicativity","author":"abel","year":"2013","journal-title":"Habilitation"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"ref22","article-title":"Homotopy canonicity for cubical type theory","volume":"131","author":"coquand","year":"2019","journal-title":"4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(75)90015-8"},{"key":"ref23","author":"crole","year":"1993","journal-title":"Categories for Types"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"ref51","article-title":"Internalizing the external, or the joys of codiscreteness","author":"shulman","year":"2011"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"ref58","article-title":"Categorical intuitions underlying semantic normalisation proofs","author":"streicher","year":"1998","journal-title":"Preliminary Proceedings of the APPSEM Workshop on Normalisation by Evaluation"},{"key":"ref57","article-title":"A cubical language for Bishop sets","author":"sterling","year":"2020"},{"key":"ref56","first-page":"31:1","article-title":"Cubical syntax for reflection-free extensional equality","volume":"131","author":"sterling","year":"0"},{"key":"ref55","article-title":"Logical Relations As Types: Proof-Relevant Parametricity for Program Modules","author":"sterling","year":"2020"},{"key":"ref54","article-title":"Lectures on Synthetic Tait Computability","author":"sterling","year":"2020"},{"key":"ref53","doi-asserted-by":"crossref","DOI":"10.1109\/LICS52264.2021.9470719","article-title":"Normalization for cubical type theory","author":"sterling","year":"2021"},{"key":"ref52","article-title":"Objective Metatheory of (Cubical) Type Theories","author":"sterling","year":"2020","journal-title":"Thesis proposal"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.2307\/2586693"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511691690"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.049"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"ref14","first-page":"23:1","article-title":"Guarded Cubical Type Theory: Path Equality for Guarded Recursion","volume":"62","author":"birkedal","year":"2016","journal-title":"25th EACSL Annual Conference on Computer Science Logic (CSL)"},{"key":"ref15","article-title":"Using the internal language of toposes in algebraic geometry","author":"blechschmidt","year":"2017","journal-title":"Ph D Dissertation"},{"key":"ref16","author":"bunge","year":"1890","journal-title":"Singular coverings of toposes"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1017\/9781108553490"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001183"},{"key":"ref19","first-page":"3127","article-title":"Cubical Type Theory: a constructive interpretation of the univalence axiom","volume":"4","author":"cohen","year":"2017","journal-title":"IfCoLog J of Logics and their Applications"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1017\/9781108854429.007"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"ref5","article-title":"Computational semantics of Cartesian cubical type theory","author":"angiuli","year":"2019","journal-title":"Ph D Dissertation"},{"key":"ref8","article-title":"Syntax and models of Cartesian cubical type theory","author":"angiuli","year":"2019"},{"key":"ref49","article-title":"Modalities in homotopy type theory","volume":"16","author":"rijke","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"ref7","first-page":"6:1","article-title":"Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities","volume":"119","author":"angiuli","year":"0"},{"key":"ref9","author":"artin","year":"1972","journal-title":"Théorie des topos et cohomologie étale des schémas"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"ref45","first-page":"24:1","article-title":"Axioms for modelling cubical type theory in a topos","author":"orton","year":"2016","journal-title":"25th EACSL Annual Conference on Computer Science Logic CSL 2016 August 29 - September 1 2016"},{"key":"ref48","doi-asserted-by":"crossref","DOI":"10.21136\/HS.2017.06","article-title":"A type theory for synthetic ?-categories","volume":"1","author":"riehl","year":"2017","journal-title":"Higher Structures"},{"key":"ref47","article-title":"${\\color{red}{\\text {red}}}{\\text{tt}}$","year":"2018"},{"key":"ref42","first-page":"22:1","article-title":"Internal universes in models of homotopy type theory","author":"licata","year":"2018","journal-title":"3rd International Conference on Formal Structures for Computation and Deduction FSCD 2018 July 9-12 2018"},{"key":"ref41","first-page":"377","article-title":"Toward the description in a smooth topos of the dynamically possible motions and deformations of a continuous body","volume":"21","author":"lawvere","year":"1980","journal-title":"Cahiers de Topologie et Géométrie Diff´ erentielle Catégoriques"},{"key":"ref44","volume":"7","author":"nordstr\u00f6m","year":"1990","journal-title":"Programming in Martin-Löf’s Type Theory"},{"key":"ref43","article-title":"Algebraic models of dependent type theory","author":"newstead","year":"2018","journal-title":"Ph D Dissertation"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Rome, Italy","start":{"date-parts":[[2021,6,29]]},"end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470719.pdf?arnumber=9470719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T02:31:57Z","timestamp":1672713117000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470719\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":66,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470719","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}