{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:55Z","timestamp":1776891475825,"version":"3.51.2"},"reference-count":49,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,10,14]],"date-time":"2021-10-14T00:00:00Z","timestamp":1634169600000},"content-version":"unspecified","delay-in-days":286,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call\n                    <jats:italic>gradual type theory<\/jats:italic>\n                    (GTT). Based on Levy\u2019s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called\n                    <jats:italic>graduality<\/jats:italic>\n                    , also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality\n                    <jats:italic>must<\/jats:italic>\n                    violate the eta equality. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.\n                  <\/jats:p>","DOI":"10.1017\/s0956796821000125","type":"journal-article","created":{"date-parts":[[2021,10,14]],"date-time":"2021-10-14T11:18:16Z","timestamp":1634210296000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Gradual type theory"],"prefix":"10.46298","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8141-195X","authenticated-orcid":false,"given":"MAX S.","family":"NEW","sequence":"first","affiliation":[]},{"given":"DANIEL R.","family":"LICATA","sequence":"additional","affiliation":[]},{"given":"AMAL","family":"AHMED","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2021,10,14]]},"reference":[{"key":"S0956796821000125_ref4","unstructured":"Boyland, J. (2014) The problem of structural type tests in a gradually typed language. In 21st Workshop on Foundations of Object-Oriented Languages."},{"key":"S0956796821000125_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3110282"},{"key":"S0956796821000125_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"S0956796821000125_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796821000125_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"S0956796821000125_ref36","unstructured":"Pitts, A. & Stark, I. (1998) Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, Gordon, A. & Pitts, A. (eds), Publications of the Newton Institute, Cambridge University Press, pp. 227\u2013273."},{"key":"S0956796821000125_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009898"},{"key":"S0956796821000125_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"S0956796821000125_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"S0956796821000125_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"S0956796821000125_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80078-1"},{"key":"S0956796821000125_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-013-9094-y"},{"key":"S0956796821000125_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"S0956796821000125_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"S0956796821000125_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_2"},{"key":"S0956796821000125_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"S0956796821000125_ref3","first-page":"1","volume-title":"Algebra and Coalgebra in Computer Science","author":"Bauer","year":"2013"},{"key":"S0956796821000125_ref28","unstructured":"Nakano, H. (2000) A modality for recursion. In IEEE Symposium on Logic in Computer Science (LICS), Santa Barbara, California."},{"key":"S0956796821000125_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"S0956796821000125_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"S0956796821000125_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_15"},{"key":"S0956796821000125_ref31","doi-asserted-by":"crossref","unstructured":"New, M. S. & Licata, D. R. (2020) Call-by-name gradual type theory. In LMCS.","DOI":"10.1017\/S0956796821000125"},{"key":"S0956796821000125_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"S0956796821000125_ref43","volume-title":"Is sound gradual typing dead? In ACM Symposium on Principles of Programming Languages (POPL)","author":"Takikawa","year":"2016"},{"key":"S0956796821000125_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3341715"},{"key":"S0956796821000125_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3290328"},{"key":"S0956796821000125_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"S0956796821000125_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009863"},{"key":"S0956796821000125_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"S0956796821000125_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3236766"},{"key":"S0956796821000125_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"S0956796821000125_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_21"},{"key":"S0956796821000125_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676967"},{"key":"S0956796821000125_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"S0956796821000125_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"S0956796821000125_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"S0956796821000125_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_26"},{"key":"S0956796821000125_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"S0956796821000125_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"S0956796821000125_ref40","unstructured":"Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Scheme and Functional Programming Workshop (Scheme), pp. 81\u201392."},{"key":"S0956796821000125_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"S0956796821000125_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"S0956796821000125_ref49","unstructured":"Zeilberger, N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. Ph.D. thesis, Carnegie Mellon University."},{"key":"S0956796821000125_ref39","unstructured":"Siek, J. , Vitousek, M. , Cimini, M. & Boyland, J. T. (2015) Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages. SNAPL 2015."},{"key":"S0956796821000125_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"S0956796821000125_ref30","unstructured":"New, M. S. & Licata, D. R. (2018) Call-by-name gradual type theory. In FSCD."},{"key":"S0956796821000125_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_17"},{"key":"S0956796821000125_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"},{"key":"S0956796821000125_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796821000125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:20:13Z","timestamp":1776889213000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000125\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":49,"alternative-id":["S0956796821000125"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000125","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e21"}}