{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:42:06Z","timestamp":1770291726596,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T00:00:00Z","timestamp":1529971200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["00012386"],"award-info":[{"award-number":["00012386"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"name":"The Danish Council for Independent Research for the Natural Sciences"},{"name":"Microsoft (US)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10817-018-9471-7","type":"journal-article","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T01:32:11Z","timestamp":1529976731000},"page":"211-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Guarded Cubical Type Theory"],"prefix":"10.1007","volume":"63","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Bizjak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranald","family":"Clouston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans Bugge","family":"Grathwohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,26]]},"reference":[{"key":"9471_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Vezzosi, A.: A formalized proof of strong normalization for guarded recursive types. In: APLAS, pp. 140\u2013158 (2014)","DOI":"10.1007\/978-3-319-12736-1_8"},{"key":"9471_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: PLPV, pp. 57\u201368 (2007)","DOI":"10.1145\/1292597.1292608"},{"key":"9471_CR3","doi-asserted-by":"crossref","unstructured":"Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197\u2013208 (2013)","DOI":"10.1145\/2544174.2500597"},{"key":"9471_CR4","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Rasmus, E.M.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213\u2013222 (2013)","DOI":"10.1109\/LICS.2013.27"},{"key":"9471_CR5","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL, pp. 119\u2013132 (2011)","DOI":"10.1145\/1925844.1926401"},{"key":"9471_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In: LMCS, vol. 8, no. 4 (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"9471_CR7","unstructured":"Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory: path equality for guarded recursion. In: CSL, vol. 3, p. 37 (2016)"},{"issue":"3","key":"9471_CR8","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1215\/S0012-7094-37-00334-X","volume":"3","author":"G Birkhoff","year":"1937","unstructured":"Birkhoff, G.: Rings of sets. Duke Math. J. 3(3), 443\u201354 (1937)","journal-title":"Duke Math. J."},{"key":"9471_CR9","doi-asserted-by":"crossref","unstructured":"Bizjak, A., M\u00f8gelberg, R.E.: A model of guarded recursion with clock synchronisation. In: MFPS, pp. 83\u2013101 (2015)","DOI":"10.1016\/j.entcs.2015.12.007"},{"key":"9471_CR10","doi-asserted-by":"crossref","unstructured":"Bizjak, A., Grathwohl, H.B., Clouston, R., M\u00f8gelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: FoSSaCS, pp. 20\u201335 (2016)","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"9471_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26","author":"R Clouston","year":"2016","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. (2016). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_26","journal-title":"Log. Methods Comput. Sci."},{"key":"9471_CR12","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: Post-proceedings of the 21st International Conference on Types for Proofs and Programs, TYPES 2015 (2016)"},{"key":"9471_CR13","unstructured":"Coquand, T.: Internal version of the uniform Kan filling condition. http:\/\/www.cse.chalmers.se\/~coquand\/shape.pdf (2015). Accessed 13 June 2018"},{"issue":"1","key":"9471_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0004972700022966","volume":"16","author":"W Cornish","year":"1977","unstructured":"Cornish, W., Fowler, P.: Coproducts of de Morgan algebras. Bull. Aust. Math. Soc. 16(1), 1\u201313 (1977)","journal-title":"Bull. Aust. Math. Soc."},{"key":"9471_CR15","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Internal type theory. In: TYPES \u201995, pp. 120\u2013134 (1996)","DOI":"10.1007\/3-540-61780-9_66"},{"key":"9471_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1","volume-title":"Extensional Constructs in Intensional Type Theory","author":"M Hofmann","year":"1997","unstructured":"Hofmann, M.: Extensional Constructs in Intensional Type Theory. Springer, Berlin (1997)"},{"key":"9471_CR17","unstructured":"Hofmann, M., Streicher, T.: Lifting Grothendieck universes. http:\/\/www.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf (1999). Accessed 13 June 2018"},{"key":"9471_CR18","unstructured":"Huber, S.: Canonicity for cubical type theory. arXiv:1607.04156 (2016)"},{"key":"9471_CR19","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"PT Johnstone","year":"2002","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press, Oxford (2002)"},{"key":"9471_CR20","unstructured":"Kapulkin, C., Lumsdaine, P.L.: The simplicial model of univalent foundations (after Voevodsky). arXiv:1211.2851 (2012)"},{"key":"9471_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8","volume-title":"Categories for the Working Mathematician","author":"S Mac\u00a0Lane","year":"1978","unstructured":"Mac\u00a0Lane, S.: Categories for the Working Mathematician, vol. 5. Springer, Berlin (1978)"},{"key":"9471_CR22","volume-title":"Sheaves in Geometry and Logic","author":"S Mac Lane","year":"1992","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, Berlin (1992)"},{"key":"9471_CR23","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Logic Colloquium \u201973, pp. 73\u2013118 (1975)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"9471_CR24","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0 (2004)"},{"issue":"1","key":"9471_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008)","journal-title":"J. Funct. Program."},{"key":"9471_CR26","doi-asserted-by":"crossref","unstructured":"M\u00f8gelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS (2014)","DOI":"10.1145\/2603088.2603132"},{"key":"9471_CR27","doi-asserted-by":"crossref","unstructured":"Nakano, H.: A modality for recursion. In: LICS, pp. 255\u2013266 (2000)","DOI":"10.1109\/LICS.2000.855774"},{"key":"9471_CR28","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. Thesis, Chalmers University of Technology (2007)"},{"key":"9471_CR29","unstructured":"Orton, I., Pitts, A.M.: Axioms for modelling cubical type theory in a topos. In: CSL (2016)"},{"key":"9471_CR30","unstructured":"Phoa, W.: An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, LFCS, University of Edinburgh (1992)"},{"key":"9471_CR31","unstructured":"Sacchini, J.L.: Well-founded sized types in the calculus of constructions. In: TYPES 2015 talk (2015) http:\/\/cs.ioc.ee\/types15\/programme-slides.html (2015). Accessed 13 June 2018"},{"key":"9471_CR32","unstructured":"Spitters, B.: Cubical sets as a classifying topos. In: TYPES (2015)"},{"key":"9471_CR33","unstructured":"The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study (2013)"},{"key":"9471_CR34","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-1-4020-5587-4_8","volume-title":"Handbook of Spatial Logics","author":"S Vickers","year":"2007","unstructured":"Vickers, S.: Locales and toposes as spaces. In: Aiello, M., Pratt-Hartmann, I.E., van Benthem, J.F.A.K. (eds.) Handbook of Spatial Logics, pp. 429\u2013496. Springer, Berlin (2007)"},{"key":"9471_CR35","unstructured":"Voevodsky, V.: Martin-Lof identity types in the C-systems defined by a universe category. arXiv:1505.06446 (2015)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9471-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9471-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9471-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T09:40:28Z","timestamp":1751708428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9471-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,26]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["9471"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9471-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,26]]},"assertion":[{"value":"20 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}