{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:55Z","timestamp":1780994575257,"version":"3.54.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"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":[[2019,1,2]]},"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 were recently proposed. Among other issues, these proposals can however signal parametricity errors in unexpected situations, and improperly handle type instantiations when imprecise types are involved. These observations further suggest that existing polymorphic cast calculi are not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challenge of designing a gradual language with explicit parametric polymorphism, exploring the extent to which the Abstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design and metatheory of GSF, and provide a reference implementation. In addition to avoiding the uncovered semantic issues, GSF satisfies all the expected properties of a gradual parametric language, save for one property: the dynamic gradual guarantee, which was left as conjecture in all prior work, is here proven to be simply incompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity.<\/jats:p>","DOI":"10.1145\/3290330","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Gradual parametricity, revisited"],"prefix":"10.1145","volume":"3","author":[{"given":"Mat\u00edas","family":"Toro","sequence":"first","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elizabeth","family":"Labrada","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","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","volume-title":"Blame for All. In Workshop on Script to Program Evolution (STOP)","author":"Ahmed Amal","year":"2009","unstructured":"Amal Ahmed , Robert Bruce Findler , Jacob Matthews , and Philip Wadler . 2009 . Blame for All. In Workshop on Script to Program Evolution (STOP) . Genova, Italy. Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. 2009. Blame for All. In Workshop on Script to Program Evolution (STOP). Genova, Italy."},{"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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_2_8_1","article-title":"Gradual Type-and-Effect Systems","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. 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 26"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1883986"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113469"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_2_12_1","volume-title":"Combinatory Logic","author":"Curry Haskell B.","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. 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_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_2_2_14_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. Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In International Workshop on Scripts to Programs."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_2_2_16_1","volume-title":"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.)","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. 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_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_18_1","unstructured":"Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. eprint arXiv:1511.01399.  Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. eprint arXiv:1511.01399."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000265"},{"key":"e_1_2_2_24_1","unstructured":"ICFP 2017 2017.  ICFP 2017 2017."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110282"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048114"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645420.652519"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792881"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_2_2_38_1","unstructured":"Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Manuscript.  Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Manuscript."},{"key":"e_1_2_2_39_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press , Cambridge, MA, USA . Benjamin C. Pierce. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103714"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647323.721503"},{"key":"e_1_2_2_42_1","volume-title":"Information Processing 83","author":"Reynolds John C.","unstructured":"John C. Reynolds . 1983. Types , abstraction, and parametric polymorphism . In Information Processing 83 , R. E. A. Mason (Ed.). Elsevier , 513\u2013523. John C. Reynolds. 1983. Types, abstraction, and parametric polymorphism. In Information Processing 83, R. E. A. Mason (Ed.). Elsevier, 513\u2013523."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888274"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_2_45_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81\u201392","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 . 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_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_48_1","volume-title":"Refined Criteria for Gradual Typing. In 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 . 2015 a. 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. 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_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_2_52_1","unstructured":"Mat\u00edas Toro Elizabeth Labrada and \u00c9ric Tanter. 2018b. Gradual Parametricity Revisited (with Appendix). arXiv:1807.04596 {cs.PL}.  Mat\u00edas Toro Elizabeth Labrada and \u00c9ric Tanter. 2018b. Gradual Parametricity Revisited (with Appendix). arXiv:1807.04596 {cs.PL}."},{"key":"e_1_2_2_53_1","volume-title":"Proceedings of the 24th Static Analysis Symposium (SAS 2017)","volume":"10422","author":"Mat\u00edas","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types . In Proceedings of the 24th Static Analysis Symposium (SAS 2017) (Lecture Notes in Computer Science) , Vol. 10422 . Springer-Verlag, New York City, NY, USA, 382\u2013404. Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types. In Proceedings of the 24th Static Analysis Symposium (SAS 2017) (Lecture Notes in Computer Science), Vol. 10422. Springer-Verlag, New York City, NY, USA, 382\u2013404."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_55_1","volume-title":"Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011)","volume":"6813","author":"Wolff Roger","year":"2011","unstructured":"Roger Wolff , Ronald Garcia , \u00c9ric Tanter , and Jonathan Aldrich . 2011 . Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011) (Lecture Notes in Computer Science), Mira Mezini (Ed.) , Vol. 6813 . Springer-Verlag, Lancaster, UK, 459\u2013483. Roger Wolff, Ronald Garcia, \u00c9ric Tanter, and Jonathan Aldrich. 2011. Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011) (Lecture Notes in Computer Science), Mira Mezini (Ed.), Vol. 6813. Springer-Verlag, Lancaster, UK, 459\u2013483."},{"key":"e_1_2_2_56_1","volume-title":"Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018)","volume":"10801","author":"Xie Ningning","unstructured":"Ningning Xie , Xuan Bi , and Bruno C . d. S. Oliveira. 2018. Consistent Subtyping for All . In Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018) (Lecture Notes in Computer Science), Amal Ahmed (Ed.) , Vol. 10801 . Springer-Verlag, Thessaloniki, Greece, 3\u201330. Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018) (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer-Verlag, Thessaloniki, Greece, 3\u201330."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290330","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290330","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290330"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290330"],"URL":"https:\/\/doi.org\/10.1145\/3290330","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}