{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T12:54:00Z","timestamp":1768827240146,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100020884","name":"Agencia Nacional de Investigaci\u00f3n y Desarrollo","doi-asserted-by":"crossref","award":["1190058, 3200583"],"award-info":[{"award-number":["1190058, 3200583"]}],"id":[{"id":"10.13039\/501100020884","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000181","name":"United States Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-21-1-0054"],"award-info":[{"award-number":["FA9550-21-1-0054"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>Graduality and parametricity have proven to be extremely challenging notions to bring together. Intuitively, enforcing parametricity gradually requires possibly sealing values in order to detect violations of uniform behavior. Toro et al. (2019) argue that the two notions are incompatible in the context of System F, where sealing is transparently driven by potentially imprecise type information, while New et al. (2020) reconcile both properties at the cost of abandoning the syntax of System F and requiring user-provided sealing annotations that are not subject to graduality guarantees. Furthermore, all current proposals rely on a global form of dynamic sealing in order to enforce parametric behavior at runtime, which weakens parametric reasoning and breaks equivalences in the static language. Based on the observation that the tension between graduality and parametricity comes from the early commitment to seal values based on type information, we propose plausible sealing as a new intermediate language mechanism that allows postponing such decisions to runtime. We propose an intermediate language for gradual parametricity, Funky, which supports plausible sealing in a simplified setting where polymorphism is restricted to instantiations with base and variable types. We prove that Funky satisfies both parametricity and graduality, mechanizing key lemmas in Agda. Additionally, we avoid global dynamic sealing and instead propose a novel lexically-scoped form of sealing realized using a representation of evidence inspired by the category of spans. As a consequence, Funky satisfies a standard formulation of parametricity that does not break System F equivalences. In order to show the practicality of plausible sealing, we describe a translation from Funk, a source language without explicit sealing, to Funky, that takes care of inserting plausible sealing forms. We establish graduality of Funk, subject to a restriction on type applications, and explain the source-level parametric reasoning it supports. Finally, we provide an interactive prototype along with illustrative examples both novel and from the literature.<\/jats:p>","DOI":"10.1145\/3527314","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Plausible sealing for gradual parametricity"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8740-5163","authenticated-orcid":false,"given":"Elizabeth","family":"Labrada","sequence":"first","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5315-0198","authenticated-orcid":false,"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_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_1_4_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. 39:1\u201339:28.  Amal Ahmed Dustin Jamner Jeremy G. Siek and Philip Wadler. 2017. Theorems for Free for Free: Parametricity with and Without Types. 39:1\u201339:28.","DOI":"10.1145\/3110283"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_6_1","first-page":"1","article-title":"Abstracting Gradual Typing Moving Forward","volume":"61","author":"Schwerter Felipe Ba\u00f1ados","year":"2021","unstructured":"Felipe Ba\u00f1ados Schwerter , Alison M. Clark , and Jafery. 2021 . Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient. 61 : 1 \u2013 61 :28. Felipe Ba\u00f1ados Schwerter, Alison M. Clark, and Jafery. 2021. Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient. 61:1\u201361:28.","journal-title":"Precise and Space-Efficient."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","year":"2016","unstructured":"2016. Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016 ), Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM Press, St Petersburg, FL, USA. 2016. Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM Press, St Petersburg, FL, USA."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Matteo Cimini and Jeremy Siek. 2016. The gradualizer: a methodology and algorithm for generating gradual type systems. 443\u2013455.  Matteo Cimini and Jeremy Siek. 2016. The gradualizer: a methodology and algorithm for generating gradual type systems. 443\u2013455.","DOI":"10.1145\/2914770.2837632"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. 429\u2013442. See erratum: https:\/\/www.cs.ubc.ca\/ rxg\/agt-erratum.pdf.  Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. 429\u2013442. See erratum: https:\/\/www.cs.ubc.ca\/ rxg\/agt-erratum.pdf.","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_1_13_1","unstructured":"2017.  2017."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Yuu Igarashi Taro Sekiyama and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. 40:1\u201340:29.  Yuu Igarashi Taro Sekiyama and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. 40:1\u201340:29.","DOI":"10.1145\/3110284"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Koen Jacobs Amin Timany and Dominique Devriese. 2021. Fully abstract from static to gradual. 7:1\u20137:30.  Koen Jacobs Amin Timany and Dominique Devriese. 2021. Fully abstract from static to gradual. 7:1\u20137:30.","DOI":"10.1145\/3434288"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","author":"Nico","year":"2017","unstructured":"Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types . In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017 ). ACM Press, Paris, France. 775\u2013788. Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017). ACM Press, Paris, France. 775\u2013788."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, ICFP","author":"Max","year":"2018","unstructured":"Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs . Proceedings of the ACM on Programming Languages, 2, ICFP ( 2018 ), Sept., 73:1\u201373:30. Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. Proceedings of the ACM on Programming Languages, 2, ICFP (2018), Sept., 73:1\u201373:30."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_1_21_1","unstructured":"nLab contributors. 2021. pullback. https:\/\/ncatlab.org\/nlab\/show\/pullback  nLab contributors. 2021. pullback. https:\/\/ncatlab.org\/nlab\/show\/pullback"},{"key":"e_1_2_1_22_1","unstructured":"nLab contributors. 2021. span. https:\/\/ncatlab.org\/nlab\/show\/span  nLab contributors. 2021. span. https:\/\/ncatlab.org\/nlab\/show\/span"},{"key":"e_1_2_1_23_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_1_24_1","unstructured":"2021.  2021."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_1_26_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_1_27_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_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_1_29_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":"293","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . 2015 . 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\u2013 293 . Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. 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_1_30_1","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL","author":"Sumii Eijiro","year":"2005","unstructured":"Eijiro Sumii and Benjamin C. Pierce . 2004. A Bisimulation for Dynamic Sealing . In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005 ). ACM Press, Venice, Italy. 161\u2013172. Eijiro Sumii and Benjamin C. Pierce. 2004. A Bisimulation for Dynamic Sealing. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005). ACM Press, Venice, Italy. 161\u2013172."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_1_32_1","volume-title":"Revisited. Proceedings of the ACM on Programming Languages, 3, POPL","author":"Toro Mat\u00edas","year":"2019","unstructured":"Mat\u00edas Toro , Elizabeth Labrada , and \u00c9ric Tanter . 2019 . Gradual Parametricity , Revisited. Proceedings of the ACM on Programming Languages, 3, POPL (2019), Jan., 17:1\u201317:30. Mat\u00edas Toro, Elizabeth Labrada, and \u00c9ric Tanter. 2019. Gradual Parametricity, Revisited. Proceedings of the ACM on Programming Languages, 3, POPL (2019), Jan., 17:1\u201317:30."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP","volume":"30","author":"Xie Ningning","year":"2018","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 ), Amal Ahmed (Ed.) (Lecture Notes in Computer Science , Vol. 10801). Springer-Verlag, Thessaloniki, Greece. 3\u2013 30 . 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), Amal Ahmed (Ed.) (Lecture Notes in Computer Science, 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\/3527314","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527314","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527314"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":32,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527314"],"URL":"https:\/\/doi.org\/10.1145\/3527314","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}