{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:57:26Z","timestamp":1787065046764,"version":"build-2736575974"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["715753"],"award-info":[{"award-number":["715753"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["390781972"],"award-info":[{"award-number":["390781972"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002301","name":"Estonian Research Council","doi-asserted-by":"crossref","award":["PSG749"],"award-info":[{"award-number":["PSG749"]}],"id":[{"id":"10.13039\/501100002301","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002347","name":"Bundesministerium f\u00fcr Bildung und Forschung","doi-asserted-by":"publisher","award":["16KISK038"],"award-info":[{"award-number":["16KISK038"]}],"id":[{"id":"10.13039\/501100002347","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":[[2024,1,2]]},"abstract":"\n We introduce SCIO\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n , a formally secure compilation framework for statically verified programs performing input-output (IO). The source language is an F\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n subset in which a verified program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n subset in which the compiled program is linked with an adversarial context that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the state of the monitor. But these checks cannot stop the adversarial target context\n before<\/jats:italic>\n it performs dangerous IO operations. Therefore linking in SCIO\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n that SCIO\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n that SCIO\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO\n \n \n \n \n \u22c6<\/mml:mo>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:inline-formula>\n at work on a simple web server example.\n <\/jats:p>","DOI":"10.1145\/3632916","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2226-2259","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Securing Verified IO Programs Against Unverified Code in F*"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7525-2440","authenticated-orcid":false,"given":"Cezar-Constantin","family":"Andrici","sequence":"first","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-4082-570X","authenticated-orcid":false,"given":"\u0218tefan","family":"Ciob\u00e2c\u0103","sequence":"additional","affiliation":[{"name":"Alexandru Ioan Cuza University, Ia?i, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8919-8081","authenticated-orcid":false,"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5831-9991","authenticated-orcid":false,"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2114-624X","authenticated-orcid":false,"given":"Exequiel","family":"Rivas","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Tallinn, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9881-3696","authenticated-orcid":false,"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"Inria Saclay, Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2023. Dafny Reference Manual. https:\/\/dafny.org\/latest\/DafnyRef\/DafnyRef"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.32"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243745"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.12"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_3_1_9_1","article-title":"CertiCoq: A verified compiler for Coq","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In 3rd Workshop on Coq for Programming Languages (CoqPL). https:\/\/popl17.sigplan.org\/details\/main\/9\/CertiCoq-A-verified-compiler-for-Coq","journal-title":"3rd Workshop on Coq for Programming Languages (CoqPL)"},{"key":"e_1_3_1_10_1","unstructured":"James Anderson. 1973. Computer Security Technology Planning Study. ESD-TR-73-51 US Air Force Electronic Systems Division (1973). Section 4.1.1 http:\/\/csrc.nist.gov\/publications\/history\/ande72.pdf. http:\/\/csrc.nist.gov\/publications\/history\/ande72.pdf"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Cezar-Constantin Andrici Stefan Ciob\u00e2c\u0103 C\u0103t\u0103lin Hri\u0163cu Guido Mart\u00ednez Exequiel Rivas \u00c9ric Tanter and Th\u00e9o Winterhalter. 2023a. Artifact for the POPL 2024 paper \u2018Securing Verified IO Programs Against Unverified Code in F*\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10125015 10.5281\/zenodo.10125015","DOI":"10.5281\/zenodo.10125015"},{"key":"e_1_3_1_12_1","unstructured":"Cezar-Constantin Andrici Stefan Ciob\u00e2c\u0103 C\u0103t\u0103lin Hri\u0163cu Guido Mart\u00ednez Exequiel Rivas \u00c9ric Tanter and Th\u00e9o Winterhalter. 2023b. Artifact for the POPL 2024 paper \u2018Securing Verified IO Programs Against Unverified Code in F*\u2019. GitHub. https:\/\/github.com\/andricicezar\/fstar-io\/tree\/popl24\/sciostar"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.8"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575687"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297070"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484588"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_25"},{"key":"e_1_3_1_21_1","first-page":"917","volume-title":"26th USENIX Security Symposium","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 917\u2013934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_36"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_6"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:2)2017"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034800"},{"key":"e_1_3_1_31_1","first-page":"201","article-title":"Trace-Based Aspects","author":"Douence R\u00e9mi","year":"2005","unstructured":"R\u00e9mi Douence, Pascal Fradet, and Mario S\u00fcdholt. 2005. Trace-Based Aspects. In Aspect-Oriented Software Development, Robert E. Filman, Tzilla Elrad, Siobh\u00e1n Clarke, and Mehmet Ak\u015fit (Eds.). Addison-Wesley, Boston, 201\u2013217. https:\/\/inria.hal.science\/inria-00000947\/fr\/","journal-title":"Aspect-Oriented Software Development"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00036"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_6"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_1_35_1","unstructured":"Matthew Flatt and PLT. [n. d.]. The Racket Reference. https:\/\/docs.racket-lang.org\/reference\/. https:\/\/docs.racket-lang.org\/reference\/"},{"key":"e_1_3_1_36_1","article-title":"A Verified, Efficient Embedding of a Verifiable Assembly Language","volume":"3","author":"Fromherz Aymeric","year":"2019","unstructured":"Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019. A Verified, Efficient Embedding of a Verifiable Assembly Language. PACMPL 3, POPL (2019). https:\/\/github.com\/project-everest\/project-everest.github.io\/raw\/master\/assets\/vale-popl.pdf","journal-title":"PACMPL"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_3_1_39_1","first-page":"653","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622823"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"e_1_3_1_42_1","article-title":"Storage Systems are Distributed Systems (So Verify Them That Way!)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). https:\/\/www.andrew.cmu.edu\/user\/bparno\/papers\/veribetrkv.pdf","journal-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.7146\/dpb.v7i86.6502"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373812"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00523-2"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527313"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36579-6_4"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984021"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103779"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_7"},{"key":"e_1_3_1_69_1","article-title":"Abstract I\/O Specification","author":"Penninckx Willem","year":"2019","unstructured":"Willem Penninckx, Amin Timany, and Bart Jacobs. 2019. Abstract I\/O Specification. CoRR abs\/1901.10541 (2019). arXiv:1901.10541 http:\/\/arxiv.org\/abs\/1901.10541","journal-title":"CoRR"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_1_72_1","first-page":"1465","volume-title":"28th USENIX Security Symposium","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association, 1465\u20131482. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_3_1_74_1","unstructured":"Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2021. Programming and Proving with Indexed Effects. https:\/\/www.fstar-lang.org\/papers\/indexedeffects\/"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.005"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100006X"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_1_80_1","unstructured":"Matthieu Sozeau Yannick Forster Meven Lennon-Bertrand Jakob Botsch Nielsen Nicolas Tabareau and Th\u00e9o Winterhalter. 2023. Correct and Complete Type Checking and Certified Erasure for Coq in Coq. (April 2023). https:\/\/inria.hal.science\/hal-04077552 working paper or preprint."},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000022"},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353482.1353503"},{"key":"e_1_3_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816710"},{"key":"e_1_3_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_29"},{"key":"e_1_3_1_88_1","article-title":"Partial Dijkstra Monads for All.","author":"Winterhalter Th\u00e9o","year":"2022","unstructured":"Th\u00e9o Winterhalter, Cezar-Constantin Andrici, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, Guido Mart\u00ednez, and Exequiel Rivas. 2022. Partial Dijkstra Monads for All. TYPES. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_18.pdf","journal-title":"TYPES"},{"key":"e_1_3_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"e_1_3_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"},{"key":"e_1_3_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632916","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:06:54Z","timestamp":1751645214000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632916"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":92,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632916"],"URL":"https:\/\/doi.org\/10.1145\/3632916","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}