{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T17:05:45Z","timestamp":1776013545003,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-1816837"],"award-info":[{"award-number":["CCF-1816837"]}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1453796"],"award-info":[{"award-number":["CCF-1453796"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,8,30]]},"DOI":"10.1145\/3609027.3609405","type":"proceedings-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:09:09Z","timestamp":1693501749000},"page":"14-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Semantic Encapsulation using Linking Types"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Patterson","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}]},{"given":"Andrew","family":"Wagner","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_3_2_1_3_1","volume-title":"Semantics of Types for Mutable State. Ph. D. Dissertation","author":"Ahmed Amal Jamil","unstructured":"Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428204"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Nick Benton. 2006. Abstracting allocation: The new new thing. In Computer Science Logic (CSL).","DOI":"10.1007\/11874683_12"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481864"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273922"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80452-9"},{"key":"e_1_3_2_1_13_1","unstructured":"Sylvain Boulm\u00e9 and Thomas Vandendorpe. 2019. Embedding Untrusted Imperative ML Oracles into Coq Verified Code. July https:\/\/hal.archives-ouvertes.fr\/hal-02062288 This preprint has been largely rewritten and integrated into Sylvain Boulm\u00e9\u2019s Habilitation in 2021 See http:\/\/www-verimag.imag.fr\/ boulme\/hdr.html."},{"key":"e_1_3_2_1_14_1","volume-title":"Symposium on Implementation and Application of Functional Languages. 131\u2013148","author":"Chakravarty Manuel MT","year":"1999","unstructured":"Manuel MT Chakravarty. 1999. C->HASKELL, or Yet Another Interfacing Tool. In Symposium on Implementation and Application of Functional Languages. 131\u2013148."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1145\/258948.258979","article-title":"Disposable memo functions","volume":"97","author":"Cook Byron","year":"1997","unstructured":"Byron Cook and John Launchbury. 1997. Disposable memo functions. In ICFP. 97, 310.","journal-title":"ICFP."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52592-0_60"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289437"},{"key":"e_1_3_2_1_21_1","unstructured":"The Rust Foundation. [n. d.]. The Rust Standard Library. https:\/\/doc.rust-lang.org\/std\/keyword.extern.html"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_3_2_1_23_1","volume-title":"Foster","author":"Furr Michael","year":"2005","unstructured":"Michael Furr and Jeffrey S. Foster. 2005. Checking Type Safety of Foreign Function Calls. 62\u201372."},{"key":"e_1_3_2_1_24_1","volume-title":"Foster","author":"Furr Michael","year":"2008","unstructured":"Michael Furr and Jeffrey S. Foster. 2008. Checking Type Safety of Foreign Function Calls."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_4"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103845.1094830"},{"key":"e_1_3_2_1_27_1","unstructured":"Unsafe Code Guidelines Working Group. [n. d.]. Unsafe Code Guidelines Reference. https:\/\/rust-lang.github.io\/unsafe-code-guidelines\/introduction.html"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_1_30_1","volume-title":"Proc. Haskell Workshop.","author":"Jones Simon Peyton","year":"1997","unstructured":"Simon Peyton Jones, Thomas Nordin, and Alastair Reid. 1997. GreenCard: a foreign-language interface for Haskell. In Proc. Haskell Workshop."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_1"},{"key":"e_1_3_2_1_32_1","volume-title":"RustBelt: Securing the Foundations of the Rust Programming Language. In ACM Symposium on Principles of Programming Languages (POPL).","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: Securing the Foundations of the Rust Programming Language. In ACM Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_1_33_1","volume-title":"A Foundation for Typed Concatenative Languages. Master\u2019s thesis","author":"Kleffner Robert","unstructured":"Robert Kleffner. 2017. A Foundation for Typed Concatenative Languages. Master\u2019s thesis. Northeastern University."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806601"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_2_1_38_1","volume-title":"University of London","author":"Levy Paul Blain","unstructured":"Paul Blain Levy. 2001. Call-by-Push-Value. Queen Mary, University of London. London, UK."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_3_2_1_44_1","first-page":"1","article-title":"Graduality and Parametricity: Together Again for the First Time","volume":"46","author":"New Max S.","year":"2020","unstructured":"Max S. New, Dustin Jamner, and Amal Ahmed. 2020. Graduality and Parametricity: Together Again for the First Time. Proceedings of the ACM on Programming Languages, 4, POPL, 46:1\u201346:32.","journal-title":"Proceedings of the ACM on Programming Languages, 4, POPL"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290328"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103779"},{"key":"e_1_3_2_1_47_1","volume-title":"Real world Haskell: Code you can believe in. \" O\u2019Reilly Media","author":"O\u2019Sullivan Bryan","unstructured":"Bryan O\u2019Sullivan, John Goerzen, and Donald Bruce Stewart. 2008. Real world Haskell: Code you can believe in. \" O\u2019Reilly Media, Inc.\"."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.12"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Daniel Patterson Andrew Wagner and Amal Ahmed. 2023. Semantic Encapsulation using Linking Types (Technical Appendix). July Available at https:\/\/dbp.io\/\u0142inebreak [0]pubs\/\u0142inebreak [0]2023\/\u0142inebreak [0]lt-tr.pdf","DOI":"10.1145\/3609027.3609405"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_3_2_1_53_1","volume-title":"Symposium on Implementation and Application of Functional Languages. 37\u201358","author":"Jones Simon Peyton","year":"1999","unstructured":"Simon Peyton Jones, Simon Marlow, and Conal Elliott. 1999. Stretching the storage manager: weak pointers and stable names in Haskell. In Symposium on Implementation and Application of Functional Languages. 37\u201358."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_3_2_1_55_1","unstructured":"LLVM Project. [n. d.]. LLVM Reference. https:\/\/www.llvm.org\/docs\/GarbageCollection.html##gcroot"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_57_1","unstructured":"Klaas Pruiksma William Chargin Frank Pfenning and Jason Reed. 2018. Adjoint logic. Unpublished manuscript April."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_8"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the 2006 IEEE International Symposium on Secure Software Engineering. 97\u2013106","author":"Tan Gang","year":"2006","unstructured":"Gang Tan, Andrew W. Appel, Srimat Chakradhar, Ravi Srivaths, Anand Raghunathan, and Daniel Wang. 2006. Safe Java Native interface. In Proceedings of the 2006 IEEE International Symposium on Secure Software Engineering. 97\u2013106."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297031"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449768"},{"key":"e_1_3_2_1_64_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Timany Amin","year":"2017","unstructured":"Amin Timany, L\u00e9o Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2017. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201328."},{"key":"e_1_3_2_1_65_1","volume-title":"19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings.","author":"Tov Jesse","year":"2010","unstructured":"Jesse Tov and Riccardo Pucella. 2010. Stateful Contracts for Affine Types. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509581"}],"event":{"name":"TyDe '23: 8th ACM SIGPLAN International Workshop on Type-Driven Development","location":"Seattle WA USA","acronym":"TyDe '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609027.3609405","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609027.3609405","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609027.3609405","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:58Z","timestamp":1750182538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609027.3609405"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":66,"alternative-id":["10.1145\/3609027.3609405","10.1145\/3609027"],"URL":"https:\/\/doi.org\/10.1145\/3609027.3609405","relation":{},"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}