{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:16:48Z","timestamp":1770272208796,"version":"3.49.0"},"reference-count":42,"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\/"}],"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>Gradually typed programming languages, which allow for soundly mixing static and dynamically typed programming styles, present a strong challenge for metatheorists. Even the simplest sound gradually typed languages feature at least recursion and errors, with realistic languages featuring furthermore runtime allocation of memory locations and dynamic type tags. Further, the desired metatheoretic properties of gradually typed languages have become increasingly sophisticated: validity of type-based equational reasoning as well as the relational property known as graduality. Many recent works have tackled verifying these properties, but the resulting mathematical developments are highly repetitive and tedious, with few reusable theorems persisting across different developments.<\/jats:p>\n                  <jats:p>In this work, we present a new denotational semantics for gradual typing developed using guarded domain theory. Guarded domain theory combines the generality of step-indexed logical relations for modeling advanced programming features with the modularity and reusability of denotational semantics. We demonstrate the feasibility of this approach with a model of a simple gradually typed lambda calculus and prove the validity of beta-eta equality and the graduality theorem for the denotational model. This model should provide the basis for a reusable mathematical theory of gradually typed program semantics. Finally, we have mechanized most of the core theorems of our development in Guarded Cubical Agda, a recent extension of Agda with support for the guarded recursive constructions we use.<\/jats:p>","DOI":"10.1145\/3704863","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"772-801","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6871-1714","authenticated-orcid":false,"given":"Eric","family":"Giovannini","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5676-1886","authenticated-orcid":false,"given":"Tingting","family":"Ding","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8141-195X","authenticated-orcid":false,"given":"Max S.","family":"New","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In 15th European Symposium on Programming ESOP 2006 Vienna Austria Vol. 3924. 69\u201383. https:\/\/doi.org\/10.1007\/11693024_6 10.1007\/11693024_6","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Robert Atkey and Conor McBride. 2013. Productive Coprogramming with Guarded Recursion. In International Conference on Functional Programming (ICFP) Boston Massachusetts. 197\u2013208. https:\/\/doi.org\/10.1145\/2500365.2500597 10.1145\/2500365.2500597","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Patrick Bahr Hans Bugge Grathwohl and Rasmus Ejlers M\u00f8gelberg. 2017. The clocks are ticking: No more delays!. In ACM\/IEEE Symposium on Logic in Computer Science (LICS) Reykjavik Iceland. https:\/\/doi.org\/10.1109\/LICS.2017.8005097 10.1109\/LICS.2017.8005097","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Magnus Baunsgaard Kristensen Rasmus Ejlers M\u00f8gelberg and Andrea Vezzosi. 2022. Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks. In ACM\/IEEE Symposium on Logic in Computer Science (LICS) Haifa Israel. https:\/\/doi.org\/10.1145\/3531130.3533359 10.1145\/3531130.3533359","DOI":"10.1145\/3531130.3533359"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Rasmus Ejlers Mogelberg Jan Schwinghammer and Kristian St\u00f8vring. 2011. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. In ACM\/IEEE Symposium on Logic in Computer Science (LICS) Toronto Canada. https:\/\/doi.org\/10.1109\/LICS.2011.16 10.1109\/LICS.2011.16","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Kristian Stowing and Jacob Thamsborg. 2009. Realizability Semantics of Parametric Polymorphism General References and Recursive Types. In Foundations of Software Science and Computational Structures Berlin. 456\u2013470. https:\/\/doi.org\/10.1007\/978-3-642-00596-1_32 10.1007\/978-3-642-00596-1_32","DOI":"10.1007\/978-3-642-00596-1_32"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. In ACM Symposium on Principles of Programming Languages (POPL) St. Petersburg Florida. https:\/\/doi.org\/10.1145\/2837614.2837632 10.1145\/2837614.2837632","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. [n. d.]. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Types for Proofs and Programs (TYPES) Tallinn Estonia. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.5 10.4230\/LIPIcs.TYPES.2015.5","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_12_2","volume-title":"Parametricity As a Notion of Uniformity in Reflexive Graphs","author":"Dunphy Brian Patrick","year":"2002","unstructured":"Brian Patrick Dunphy. 2002. Parametricity As a Notion of Uniformity in Reflexive Graphs. Ph. D. Dissertation. University of Illinois at Urbana-Champaign, Champaign, IL, USA. Advisor(s) Reddy, Uday."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.14288\/1.0428823"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL) St. Petersburg Florida. 429\u2013442. https:\/\/doi.org\/10.1145\/2837614.2837670 10.1145\/2837614.2837670","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Eric Giovannini Tingting Ding and Max S. New. 2024. Agda Formalization for \"Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory\". https:\/\/doi.org\/10.5281\/zenodo.13937336 10.5281\/zenodo.13937336","DOI":"10.5281\/zenodo.13937336"},{"key":"e_1_3_2_17_2","unstructured":"Eric Giovannini Tingting Ding and Max S. New. 2024. Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version). arXiv:2411.12822 [cs.PL] https:\/\/arxiv.org\/abs\/2411.12822"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523430"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3495528"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80568-1"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Rasmus Ejlers M\u00f8gelberg and Marco Paviotti. 2016. Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory. In ACM\/IEEE Symposium on Logic in Computer Science (LICS) New York City New York. https:\/\/doi.org\/10.1145\/2933575.2934516 10.1145\/2933575.2934516","DOI":"10.1145\/2933575.2934516"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290317"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"E. Moggi. 1989. Computational lambda-calculus and monads. In IEEE Symposium on Logic in Computer Science (LICS)Pacific Grove California. 14\u201323. https:\/\/doi.org\/10.1109\/LICS.1989.39155 10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"H. Nakano. 2000. A modality for recursion. In ACM\/IEEE Symposium on Logic in Computer Science (LICS) Santa Barbara California. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Georg Neis Derek Dreyer and Andreas Rossberg. 2009. Non-Parametric Parametricity. In International Conference on Functional Programming (ICFP) Edinburgh Scotland. 135\u2013148. https:\/\/doi.org\/10.1145\/1596550.1596572 10.1145\/1596550.1596572","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622860"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Max S. New and Daniel R. Licata. 2018. Call-by-name Gradual Type Theory. In Formal Structures for Computation and Deduction Oxford England. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.24 10.4230\/LIPIcs.FSCD.2018.24","DOI":"10.4230\/LIPIcs.FSCD.2018.24"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290328"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Michael Shulman. 2007. Framed bicategories and monoidal fibrations. Theory and Applications of Categories 20 (06 2007).","DOI":"10.70930\/tac\/2m83wy59"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000241"},{"key":"e_1_3_2_36_2","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81\u201392."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) Vol. 32. 274\u2013293. https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2015.274 10.4230\/LIPIcs.SNAPL.2015.274","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704884"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2210.02169"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs. In Dynamic Languages Symposium (DLS). 964\u2013974.","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In ACM Symposium on Principles of Programming Languages (POPL) San Francisco California.","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Niccol\u00f2 Veltri and Andrea Vezzosi. 2020. Formalizing \u03c0-Calculus in Guarded Cubical Agda. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) (New Orleans LA USA). 270\u2013283. https:\/\/doi.org\/10.1145\/3372885.3373814 10.1145\/3372885.3373814","DOI":"10.1145\/3372885.3373814"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Michael M. Vitousek Cameron Swords and Jeremy G. Siek. 2017. Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. In ACM Symposium on Principles of Programming Languages (POPL) Paris France. https:\/\/doi.org\/10.1145\/3009837.3009849 10.1145\/3009837.3009849","DOI":"10.1145\/3009837.3009849"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704863","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:01Z","timestamp":1770200221000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704863"],"URL":"https:\/\/doi.org\/10.1145\/3704863","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","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"}}]}}