{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:13Z","timestamp":1779836713630,"version":"3.53.1"},"reference-count":67,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,11,11]],"date-time":"2021-11-11T00:00:00Z","timestamp":1636588800000},"content-version":"unspecified","delay-in-days":314,"URL":"https:\/\/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                    The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek &amp; Taha (2006) and its underlying cast calculus. For example, Wadler and Findler (2009) added blame tracking, Siek\n                    <jats:italic>et al<\/jats:italic>\n                    . (2009) investigated alternate cast evaluation strategies, and Herman\n                    <jats:italic>et al<\/jats:italic>\n                    . (2010) replaced casts with coercions for space efficiency. The meta-theory for the GTLC has also expanded beyond type safety to include blame safety (Tobin-Hochstadt &amp; Felleisen, 2006), space consumption (Herman\n                    <jats:italic>et al<\/jats:italic>\n                    ., 2010), and the gradual guarantees (Siek\n                    <jats:italic>et al<\/jats:italic>\n                    ., 2015). These results have been proven for some variations of the GTLC but not others. Furthermore, researchers continue to develop variations on the GTLC, but establishing all of the meta-theory for new variations is time-consuming. This article identifies abstractions that capture similarities between many cast calculi in the form of two parameterized cast calculi, one for the purposes of language specification and the other to guide space-efficient implementations. The article then develops reusable meta-theory for these two calculi, proving type safety, blame safety, the gradual guarantees, and space consumption. Finally, the article instantiates this meta-theory for eight cast calculi including five from the literature and three new calculi. All of these definitions and theorems, including the two parameterized calculi, the reusable meta-theory, and the eight instantiations, are mechanized in Agda making extensive use of module parameters and dependent records to define the abstractions.\n                  <\/jats:p>","DOI":"10.1017\/s0956796821000241","type":"journal-article","created":{"date-parts":[[2021,11,11]],"date-time":"2021-11-11T05:30:01Z","timestamp":1636608601000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":4,"title":["Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9894-4856","authenticated-orcid":false,"given":"JEREMY G.","family":"SIEK","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"TIANYU","family":"CHEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,11,11]]},"reference":[{"key":"S0956796821000241_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"S0956796821000241_ref44","unstructured":"Siek, J. G. & Vitousek, M. M. (2013) Monotonic references for gradual typing. CoRR, abs\/1312.0694."},{"key":"S0956796821000241_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"S0956796821000241_ref24","unstructured":"Gronski, J. , Knowles, K. , Tomb, A. , Freund, S. N. & Flanagan, C. (2006) Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pp. 93\u2013104."},{"key":"S0956796821000241_ref41","volume-title":"Gradual Typing: Isabelle\/Isar Formalization","author":"Siek","year":"2006"},{"key":"S0956796821000241_ref48","unstructured":"Siek, J. G. , Vitousek, M. M. , Cimini, M. & Boyland, J. T. (May 2015b) Refined criteria for gradual typing. In SNAPL: Summit on Advances in Programming Languages, LIPIcs: Leibniz International Proceedings in Informatics."},{"key":"S0956796821000241_ref46","first-page":"17","volume-title":"European Symposium on Programming, ESOP","author":"Siek","year":"2009"},{"key":"S0956796821000241_ref13","unstructured":"Chung, B. , Li, P. , Nardelli, F. Z. & Vitek, J. (2018) KafKa: Gradual typing for objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018), Millstein, T. (ed), vol. 109. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, pp. 12:1\u201312:24. ISBN 978-3-95977-079-8. doi: 10.4230\/LIPIcs.ECOOP.2018.12. Available at: http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/9217."},{"key":"S0956796821000241_ref27","doi-asserted-by":"crossref","unstructured":"Herman, D. , Tomb, A. & Flanagan, C. (2010) Space-efficient gradual typing. Higher-Order Symb. Comput. 230 (2), 0 167\u2013189.","DOI":"10.1007\/s10990-011-9066-z"},{"key":"S0956796821000241_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"S0956796821000241_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2661103.2661112"},{"key":"S0956796821000241_ref32","unstructured":"Lu, K.-C. , Siek, J. G. & Kuhlenschmidt, A. (2020). Hypercoercions and a framework for equivalence of cast calculi. In Workshop on Gradual Typing."},{"key":"S0956796821000241_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"S0956796821000241_ref12","unstructured":"Chaudhuri, A. Flow: A static type checker for Javascript. Available at: http:\/\/flowtype.org\/"},{"key":"S0956796821000241_ref21","unstructured":"Greenman, B. (November 2020) Deep and Shallow Types. PhD thesis, Northeastern University."},{"key":"S0956796821000241_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"S0956796821000241_ref64","unstructured":"Wadler, P. & Findler, R. B. (2007) Well-typed programs can\u2019t be blamed. In Workshop on Scheme and Functional Programming, pp. 15\u201326."},{"key":"S0956796821000241_ref28","volume-title":"The Formulae-as-Types Notion of Construction","author":"Howard","year":"1980"},{"key":"S0956796821000241_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"S0956796821000241_ref50","unstructured":"Takikawa, A. (April 2016) The Design, Implementation, and Evaluation of a Gradual Type System for Dynamic Class Composition. PhD thesis, Northeastern University."},{"key":"S0956796821000241_ref15","unstructured":"Felleisen, M. & Friedman, D. P. (1986) Control operators, the SECD-machine and the lambda-calculus, pp. 193\u2013217."},{"key":"S0956796821000241_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"S0956796821000241_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"S0956796821000241_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3359619.3359742"},{"key":"S0956796821000241_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"S0956796821000241_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"S0956796821000241_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384674"},{"key":"S0956796821000241_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706342"},{"key":"S0956796821000241_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"S0956796821000241_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_1"},{"key":"S0956796821000241_ref31","unstructured":"Lu, K.-C. (April 2020) Equivalence of Cast Representations in Gradual Typing. Master\u2019s thesis, Indiana University."},{"key":"S0956796821000241_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0956796821000241_ref39","unstructured":"Siek, J. G. & Taha, W. (2006a) Gradual typing for functional languages. In Scheme and Functional Programming Workshop, pp. 81\u201392."},{"key":"S0956796821000241_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3236766"},{"key":"S0956796821000241_ref8","unstructured":"Bracha, G. (2004) Pluggable type systems. In OOPSLA\u201904 Workshop on Revival of Dynamic Languages."},{"key":"S0956796821000241_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/165854.165893"},{"key":"S0956796821000241_ref59","unstructured":"Vitek, J. (2016) Gradual types for real-world objects. In Script To Program Evolution Workshop, STOP."},{"key":"S0956796821000241_ref62","unstructured":"Vitousek, M. M. & Siek, J. G. (October 206b) Gradual Typing in An Open World. Technical Report TR729, Indiana University."},{"key":"S0956796821000241_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500603"},{"key":"S0956796821000241_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"S0956796821000241_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3162066"},{"key":"S0956796821000241_ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"S0956796821000241_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3434342"},{"key":"S0956796821000241_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"S0956796821000241_ref26","unstructured":"Herman, D. , Tomb, A. & Flanagan, C. (2007) Space-efficient gradual typing. In Trends in Functional Prog. (TFP), p. XXVIII."},{"key":"S0956796821000241_ref30","unstructured":"Lennon-Bertrand, M. , Maillard, K. , Tabareau, N. & Tanter, \u00c9. (2020) Gradualizing the Calculus of Inductive Constructions."},{"key":"S0956796821000241_ref37","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow","year":"2007"},{"key":"S0956796821000241_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"S0956796821000241_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"S0956796821000241_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2543728.2543742"},{"key":"S0956796821000241_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"S0956796821000241_ref53","unstructured":"The Coq Dev. Team. (April 2004) The Coq Proof Assistant Reference Manual \u2013 Version V8.0. Available at: http:\/\/coq.inria.fr."},{"key":"S0956796821000241_ref55","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"S0956796821000241_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"S0956796821000241_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"S0956796821000241_ref58","unstructured":"Verlaguet, J. & Menghrajani, A. Hack: A new programming langauge for HHVM. Available at: https:\/\/code.facebook.com\/posts\/264544830379293\/hack-a-new-programming-language-for-hhvm\/"},{"key":"S0956796821000241_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"S0956796821000241_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2617548.2617553"},{"key":"S0956796821000241_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"S0956796821000241_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2508168.2508171"},{"key":"S0956796821000241_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3325989"},{"key":"S0956796821000241_ref40","unstructured":"Siek, J. G. & Taha, W. (December 2006b). Gradual Typing for Objects: Isabelle Formaliztaion. Technical Report CU-CS-1021-06, Boulder, CO: University of Colorado."},{"key":"S0956796821000241_ref42","doi-asserted-by":"crossref","unstructured":"Siek, J. G. & Taha, W. (August 2007) Gradual typing for objects. In European Conference on Object-Oriented Programming, vol. 4609. LNCS, pp. 2\u201327.","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"S0956796821000241_ref61","unstructured":"Vitousek, M. , Swords, C. & Siek, J. G. (2017) Big types in little runtime. In Symposium on Principles of Programming Languages, POPL."},{"key":"S0956796821000241_ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03044-5_5"},{"key":"S0956796821000241_ref60","unstructured":"Vitousek, M. & Siek, J. (2016a) From optional to gradual typing via transient checks. In Script To Program Evolution Workshop, STOP."},{"key":"S0956796821000241_ref19","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\/S0956796821000241","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:04Z","timestamp":1779834904000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000241\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":67,"alternative-id":["S0956796821000241"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000241","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 (https:\/\/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":"e30"}}