{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:09Z","timestamp":1751662869154,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP17H01723"],"award-info":[{"award-number":["JP17H01723"]}],"id":[{"id":"10.13039\/501100001691","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":[[2017,8,29]]},"abstract":"<jats:p>\n            We study an extension of gradual typing\u2014a method to integrate dynamic typing and static typing smoothly in a single language\u2014to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee\u2014the so-called refined criteria, advocated by Siek et al. We develop System F\n            <jats:sub>\n              <jats:italic>G<\/jats:italic>\n            <\/jats:sub>\n            , which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F\n            <jats:sub>\n              <jats:italic>C<\/jats:italic>\n            <\/jats:sub>\n            , which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F\n            <jats:sub>\n              <jats:italic>G<\/jats:italic>\n            <\/jats:sub>\n            and System F\n            <jats:sub>\n              <jats:italic>C<\/jats:italic>\n            <\/jats:sub>\n            , geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F\n            <jats:sub>\n              <jats:italic>G<\/jats:italic>\n            <\/jats:sub>\n            satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.\n          <\/jats:p>","DOI":"10.1145\/3110284","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["On polymorphic gradual typing"],"prefix":"10.1145","volume":"1","author":[{"given":"Yuu","family":"Igarashi","sequence":"first","affiliation":[{"name":"Kyoto University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"IBM Research, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi Luca Cardelli Benjamin Pierce and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. 13 2 (1991) 237\u2013268.  Mart\u00edn Abadi Luca Cardelli Benjamin Pierce and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. 13 2 (1991) 237\u2013268.","DOI":"10.1145\/103135.103138"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1570506.1570507"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_2_6_1","unstructured":"Amal Ahmed James T. Perconti Jeremy G. Siek and Philip Wadler. 2013. Blame for All (revised). (2013).  Amal Ahmed James T. Perconti Jeremy G. Siek and Philip Wadler. 2013. Blame for All (revised). (2013)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_2"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"volume-title":"ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings. 76\u2013100","year":"2010","author":"Bierman Gavin M.","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/3089528.3089532"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009863"},{"key":"e_1_2_2_15_1","unstructured":"Facebook. 2017. The Hack Programming Language. (2017). http:\/\/hacklang.org\/.  Facebook. 2017. The Hack Programming Language. (2017). http:\/\/hacklang.org\/."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"volume-title":"Universit\u00e9 Paris VII. Summary in Proceedings of the Second Scandinavian Logic Symposium (J.E. Fenstad, editor), North-Holland","year":"1972","author":"Girard Jean-Yves","key":"e_1_2_2_19_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"volume-title":"Scheme and Functional Programming Workshop.","year":"2006","author":"Gronski Jessica","key":"e_1_2_2_21_1"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048114"},{"volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP","year":"2008","author":"Matthews Jacob","key":"e_1_2_2_24_1"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"volume-title":"Dynamic Typing When Needed: The End of the Cold War Between Programming Languages. In OOPSLA\u201904 Workshop on Revival of Dynamic Languages.","year":"2004","author":"Meijer Erik","key":"e_1_2_2_26_1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"James H. Morris Jr. 1973. Protection in Programming Languages. 16 1 (Jan. 1973) 15\u201321.  James H. Morris Jr. 1973. Protection in Programming Languages. 16 1 (Jan. 1973) 15\u201321.","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000165"},{"key":"e_1_2_2_29_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press Chapter 23.  Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press Chapter 23."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_31_1","article-title":"Polymorphic Manifest Contracts","volume":"39","author":"Sekiyama Taro","year":"2017","journal-title":"Revised and Resolved. ACM Trans. Program. Lang. Syst."},{"volume-title":"Gradual Typing for Functional Languages. In Scheme And Functional Programming Workshop. 81\u201392","author":"Jeremy","key":"e_1_2_2_32_1"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_37_1","unstructured":"Jeremy G. Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (2016).  Jeremy G. Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (2016)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96747"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661101"},{"volume-title":"SNAPL 2015","year":"2015","author":"Wadler Philip","key":"e_1_2_2_42_1"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110284","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110284","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":42,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110284"],"URL":"https:\/\/doi.org\/10.1145\/3110284","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}