{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T15:53:24Z","timestamp":1768838004315,"version":"3.49.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T00:00:00Z","timestamp":1666915200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANID\/FONDECYT","award":["1190058, and 3200583"],"award-info":[{"award-number":["1190058, and 3200583"]}]},{"name":"ANID\/Doctorado Nacional","award":["2015-21150510, and 21151566"],"award-info":[{"award-number":["2015-21150510, and 21151566"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs have been recently proposed, with varying syntax, behavior, and properties. Starting from a detailed review of the challenges and tensions that affect the design of gradual parametric languages, this work presents an extensive account of the semantics and metatheory of GSF, a gradual counterpart of System\u00a0F. In doing so, we also report on the extent to which the Abstracting Gradual Typing methodology can help us derive such a language. Among gradual parametric languages that follow the syntax of System\u00a0F, GSF achieves a unique combination of properties. We clearly establish the benefits and limitations of the language, and discuss several extensions of GSF towards a practical programming language.<\/jats:p>","DOI":"10.1145\/3555986","type":"journal-article","created":{"date-parts":[[2022,8,10]],"date-time":"2022-08-10T12:20:09Z","timestamp":1660134009000},"page":"1-78","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Gradual System F"],"prefix":"10.1145","volume":"69","author":[{"given":"Elizabeth","family":"Labrada","sequence":"first","affiliation":[{"name":"PLEIAD Lab, Computer ScienceDepartment, University of Chile, Santiago, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[{"name":"PLEIAD Lab, Computer ScienceDepartment, University of Chile, Santiago, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"PLEIAD Lab, Computer ScienceDepartment, University of Chile, Santiago, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,28]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_2_6_1","volume-title":"Workshop on Script to Program Evolution (STOP)","author":"Ahmed Amal","year":"2009","unstructured":"Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. 2009b. Blame for all. In Workshop on Script to Program Evolution (STOP). Genova, Italy."},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_3_2_8_1","doi-asserted-by":"crossref","unstructured":"Amal Ahmed Dustin Jamner Jeremy G. Siek and Philip Wadler. 2017. Theorems for free for free: Parametricity with and without types. See ICFP 2017 [2017] 39:1\u201339:28.","DOI":"10.1145\/3110283"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394778"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"e_1_3_2_11_1","first-page":"283","volume-title":"Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014)","author":"Schwerter Felipe Ba\u00f1ados","year":"2014","unstructured":"Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. 2014. A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014). ACM Press, Gothenburg, Sweden, 283\u2013295."},{"key":"e_1_3_2_12_1","first-page":"19:1\u201319:69","article-title":"Gradual type-and-effect systems","volume":"26","author":"Schwerter Felipe Ba\u00f1ados","year":"2016","unstructured":"Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. 2016. Gradual type-and-effect systems. Journal of Functional Programming 26 (Sept. 2016), 19:1\u201319:69.","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_2_13_1","first-page":"76","volume-title":"Proceedings of the 24th European Conference on Object-oriented Programming (ECOOP 2010) (Lecture Notes in Computer Science)","author":"Bierman Gavin","year":"2010","unstructured":"Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding dynamic types to C \\( ^{\\#} \\) . In Proceedings of the 24th European Conference on Object-oriented Programming (ECOOP 2010) (Lecture Notes in Computer Science), Theo D\u2019Hondt (Ed.). Springer-Verlag, Maribor, Slovenia, 76\u2013100."},{"key":"e_1_3_2_14_1","volume-title":"Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)","author":"Bod\u00edk Rastislav","year":"2016","unstructured":"Rastislav Bod\u00edk and Rupak Majumdar (Eds.). 2016. Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016). ACM Press, St. Petersburg, FL, USA."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113469"},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. See ICFP 2017 [2017] 41:1\u201341:28.","DOI":"10.1145\/3110285"},{"key":"e_1_3_2_17_1","doi-asserted-by":"crossref","unstructured":"Matteo Cimini and Jeremy Siek. 2016. The gradualizer: A methodology and algorithm for generating gradual type systems See Bod\u00edk and Majumdar [2016] 443\u2013455.","DOI":"10.1145\/2914770.2837632"},{"key":"e_1_3_2_18_1","series-title":"Studies in logic and the foundations of mathematics","volume-title":"Combinatory Logic, Volume II","author":"Curry Haskell B.","year":"1972","unstructured":"Haskell B. Curry, J. Roger Hindley, and J. P. Seldin. 1972. Combinatory Logic, Volume II. Studies in logic and the foundations of mathematics, Vol. 65. North-Holland Pub. Co."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_3_2_21_1","volume-title":"International Workshop on Scripts to Programs","author":"Disney Tim","year":"2011","unstructured":"Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In International Workshop on Scripts to Programs."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_3_2_24_1","first-page":"9:1\u20139:26","volume-title":"Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP 2016) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"56","author":"Fennell Luminous","year":"2016","unstructured":"Luminous Fennell and Peter Thiemann. 2016. LJGS: Gradual security types for object-oriented languages. In Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Rome, Italy, 9:1\u20139:26."},{"key":"e_1_3_2_25_1","doi-asserted-by":"crossref","unstructured":"Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting gradual typing. See Bod\u00edk and Majumdar [2016] 429\u2013442. See erratum https:\/\/www.cs.ubc.ca\/rxg\/agt-erratum.pdf.","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_3_2_26_1","unstructured":"Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. eprint arXiv:1511.01399."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_3_2_28_1","volume-title":"Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de l\u2019Arithm\u00e9tique d\u2019Ordre Sup\u00e9rieur","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de l\u2019Arithm\u00e9tique d\u2019Ordre Sup\u00e9rieur. Ph.D. Dissertation. Universit\u00e9 de Paris VII, Paris, France."},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2431407"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_2_32_1","first-page":"1:1\u20131:24","article-title":"Correctness of compiling polymorphism to dynamic typing","volume":"27","author":"Hou Kuen-Bang","year":"2016","unstructured":"Kuen-Bang Hou, Nick Benton, and Robert Harper. 2016. Correctness of compiling polymorphism to dynamic typing. Journal of Functional Programming 27 (2016), 1:1\u20131:24.","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_2_33_1","unstructured":"ICFP 2017 2017."},{"key":"e_1_3_2_34_1","doi-asserted-by":"crossref","unstructured":"Atsushi Igarashi Peter Thiemann Vasco T. Vasconcelos and Philip Wadler. 2017b. Gradual session types. See ICFP 2017 [2017] 38:1\u201338:28.","DOI":"10.1145\/3110282"},{"key":"e_1_3_2_35_1","doi-asserted-by":"crossref","unstructured":"Yuu Igarashi Taro Sekiyama and Atsushi Igarashi. 2017a. On polymorphic gradual typing. See ICFP 2017 [2017] 40:1\u201340:29.","DOI":"10.1145\/3110284"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048114"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527314"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_20"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_2"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_3_2_48_1","doi-asserted-by":"crossref","unstructured":"Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. 73:1\u201373:30 pages.","DOI":"10.1145\/3236768"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_2_51_1","volume-title":"Oxford Advanced Learner\u2019s Dictionary (10th ed.)","year":"2021","unstructured":"Oxford. 2021. Oxford Advanced Learner\u2019s Dictionary (10th ed.). Oxford University Press. Evidence."},{"key":"e_1_3_2_52_1","article-title":"Relating Cryptography and Polymorphism","author":"Pierce Benjamin","year":"2000","unstructured":"Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Manuscript.","journal-title":"Manuscript"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103714"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_3_2_56_1","first-page":"513","volume-title":"Information Processing 83","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction, and parametric polymorphism. In Information Processing 83, R. E. A. Mason (Ed.). Elsevier, 513\u2013523."},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888274"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_3_2_59_1","first-page":"81","volume-title":"Proceedings of the Scheme and Functional Programming Workshop","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_3_2_62_1","first-page":"274","volume-title":"1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"32","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 32. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Asilomar, California, USA, 274\u2013293."},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_3_2_64_1","unstructured":"Jeremy G. Siek and Philip Wadler. 2016. The Key to Blame: Gradual Typing Meets Cryptography. Unpublished manuscript."},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_19"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"issue":"1","key":"e_1_3_2_72_1","first-page":"5","article-title":"Abstract data types without the types","volume":"23","author":"Wadler Philip","year":"2017","unstructured":"Philip Wadler. 2017. Abstract data types without the types. Journal of Universal Computer Science 23, 1 (2017), 5\u201320.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_22"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_1"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555986","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3555986","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:41Z","timestamp":1750186961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,28]]},"references-count":75,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3555986"],"URL":"https:\/\/doi.org\/10.1145\/3555986","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,28]]},"assertion":[{"value":"2020-05-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-06-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}