{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:00:13Z","timestamp":1770246013688,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","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":[[2025,1,7]]},"abstract":"<jats:p>We present a novel analysis of the fundamental L\u00f6b induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive L\u00f6b induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside L\u00f6b induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.<\/jats:p>","DOI":"10.1145\/3704866","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"864-892","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Modal Deconstruction of L\u00f6b Induction"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1944-0789","authenticated-orcid":false,"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Frederik Lerbjerg Aagaard Magnus Baunsgaard Kristensen Daniel Gratzer and Lars Birkedal. 2022. Unifying cubical and multimodal type theory. arXiv:2203.13000 [cs.LO]"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90045-6"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9471-7"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_2_11_2","unstructured":"Ale\u0161 Bizjak and Lars Birkedal. 2022. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. Online. https:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_8"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129520000080"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.14"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"e_1_3_2_17_2","unstructured":"Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. 2017. Cubical Type Theory: a constructive interpretation of the univalence axiom. 4 10 (2017) 3127\u20133169. arXiv:https:\/\/arxiv.org\/abs\/1611.02108 [cs.LO]"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2017.02.013"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_20_2","volume-title":"Syntax and semantics of modal type theory","author":"Gratzer Daniel","year":"2023","unstructured":"Daniel Gratzer. 2023. Syntax and semantics of modal type theory. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.3"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_3_2_25_2","article-title":"Displayed Type Theory and Semi-Simplicial Types","author":"Kolomatskaia Astra","year":"2023","unstructured":"Astra Kolomatskaia and Michael Shulman. 2023. Displayed Type Theory and Semi-Simplicial Types. arXiv:2311.18781","journal-title":"arXiv:2311.1878"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533359"},{"key":"e_1_3_2_27_2","first-page":"22:1","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Licata Daniel R.","year":"2018","unstructured":"Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), H. Kirchner (Ed.). Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, 22:1\u201322:17. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.22 arXiv:1801.07664 10.4230\/LIPIcs.FSCD.2018.22 arXiv:1801.07664"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400830558"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(4:17)2020"},{"key":"e_1_3_2_31_2","unstructured":"Per Martin-L\u00f6f. 1992. Substitution calculus. Notes from a lecture given in G\u00f6teborg."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934516"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.351.13"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Rasmus Ejlers M\u00f8gelberg. 2014. A Type Theory for Productive Coprogramming via Guarded Recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS \u201914). https:\/\/doi.org\/10.1145\/2603088.2603132 10.1145\/2603088.2603132","DOI":"10.1145\/2603088.2603132"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Rasmus Ejlers M\u00f8gelberg and Niccol\u00f2 Veltri. 2019. Bisimulation as Path Type for Guarded Recursive Types. Proceedings of the ACM on Programming Languages 3 POPL (12 2019). https:\/\/doi.org\/10.1145\/3290317 10.1145\/3290317","DOI":"10.1145\/3290317"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Daniele Palombi and Jonathan Sterling. 2023. Classifying topoi in synthetic guarded domain theory. In Proceedings 38th Conference on Mathematical Foundations of Programming Semantics MFPS 2022. https:\/\/doi.org\/10.46298\/entics.10323 10.46298\/entics.10323","DOI":"10.46298\/entics.10323"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Marco Paviotti Rasmus Ejlers M\u00f8gelberg and Lars Birkedal. 2015. A Model of PCF in Guarded Type Theory. Electronic Notes in Theoretical Computer Science 319 Supplement C (2015) 333\u2013349. https:\/\/doi.org\/10.1016\/j.entcs.2015.12.020 10.1016\/j.entcs.2015.12.020 The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).","DOI":"10.1016\/j.entcs.2015.12.020"},{"issue":"1","key":"e_1_3_2_40_2","article-title":"Modalities in homotopy type theory","volume":"16","author":"Rijke Egbert","year":"2020","unstructured":"Egbert Rijke, Michael Shulman, and Bas Spitters. 2020. Modalities in homotopy type theory. Logical Methods in Computer Science 16, 1 (2020). arXiv:1706.07526","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_3_2_42_2","article-title":"All (\u221e, 1)-toposes have strict univalent universes","author":"Shulman Michael","year":"2019","unstructured":"Michael Shulman. 2019. All (\u221e, 1)-toposes have strict univalent universes. arXiv:1904.07004 [math.AT]","journal-title":"arXiv:1904.07004 [math.AT]"},{"key":"e_1_3_2_43_2","unstructured":"Michael Shulman. 2023. Towards third generation HoTT. Joint work with Thorsten Altenkirch and Ambrus Kaposi. Slides available at https:\/\/home.sandiego.edu\/~shulman\/papers\/hott-cmu-day1.pdf."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_46_2","article-title":"Denotational semantics of general store and polymorphism","author":"Sterling Jonathan","year":"2023","unstructured":"Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. 2023. Denotational semantics of general store and polymorphism. arXiv:2210.02169 [cs.PL]","journal-title":"arXiv:2210.02169 [cs.PL]"},{"key":"e_1_3_2_47_2","unstructured":"Jonathan Sterling Daniel Gratzer and Lars Birkedal. 2024. Towards univalent reference types. In Computer Science Logic (CSL 2018)."},{"key":"e_1_3_2_48_2","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_2_49_2","doi-asserted-by":"crossref","unstructured":"Niccol\u00f2 Veltri and Andrea Vezzosi. 2020. Formalizing \u03c0-calculus in guarded cubical Agda. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 270\u2013283.","DOI":"10.1145\/3372885.3373814"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Andrea Vezzosi Anders M\u00f6rtberg and Andreas Abel. 2021. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming 31 (2021). https:\/\/doi.org\/10.1017\/s0956796821000034 10.1017\/s0956796821000034","DOI":"10.1017\/s0956796821000034"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704866","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704866","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:18Z","timestamp":1770200238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704866"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704866"],"URL":"https:\/\/doi.org\/10.1145\/3704866","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}