{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:21:42Z","timestamp":1760059302756,"version":"build-2065373602"},"reference-count":118,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>In today\u2019s complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential effects of calls to external code, even though that code is not trusted and may not even be available.<\/jats:p>\n          <jats:p>The effects of external calls can be limited if internal code is programmed defensively, limiting potential effects by limiting access to the capabilities necessary to cause those effects.<\/jats:p>\n          <jats:p>This paper addresses the specification and verification of internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for access to capabilities, new specifications for limiting effects, and a Hoare logic to verify that a module satisfies its specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.<\/jats:p>","DOI":"10.1145\/3763064","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"386-415","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about External Calls"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1993-1142","authenticated-orcid":false,"given":"Sophia","family":"Drossopoulou","sequence":"first","affiliation":[{"name":"Imperial College, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3098-3901","authenticated-orcid":false,"given":"Julian","family":"Mackay","sequence":"additional","affiliation":[{"name":"Kry10 Ltd, Wellington, New Zealand"},{"name":"Victoria University, Wellington, New Zealand"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9072-6689","authenticated-orcid":false,"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[{"name":"Imperial College, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"additional","affiliation":[{"name":"Creative Research &amp; Programming, Wellington, New Zealand"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Actors: A Conceptual Foundation for Concurrent Object-Oriented Programming. In Research Directions in Object-Oriented Programming, Bruce D","author":"Agha Gul","year":"1987","unstructured":"Gul Agha and Carl Hewitt. 1987. Actors: A Conceptual Foundation for Concurrent Object-Oriented Programming. In Research Directions in Object-Oriented Programming, Bruce D. Shriver and Peter Wegner (Eds.). MIT Press, 49\u201374."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3178836"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00037"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632916"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2004.3.6.A2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Mike Barnett Rustan Leino and Wolfram Schulte. 2005. The Spec\u266f Programming System: An Overview. In CASSIS. LNCS3362 49\u201369. https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3 10.1007\/978-3-540-30569-9_3","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Jesper Bengtson Kathiekeyan Bhargavan Cedric Fournet Andrew Gordon and S.Maffeis. 2011. Refinement Types for Secure Implementations. TOPLAS 1\u2013\u00a045. https:\/\/doi.org\/10.1145\/1890028.1890031 10.1145\/1890028.1890031","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Andrew Black Kim Bruce Michael Homer and James Noble. 2012. Grace: the Absence of (Inessential) Difficulty. In Onwards. 85\u201398. https:\/\/doi.org\/10.1145\/2384592.2384601 10.1145\/2384592.2384601","DOI":"10.1145\/2384592.2384601"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Chandrasekhar Boyapati Barbara Liskov and Liuba Shrira. 2003. Ownership types for object encapsulation. In POPL. 213\u2013223. https:\/\/doi.org\/10.1145\/604131.604156 10.1145\/604131.604156","DOI":"10.1145\/604131.604156"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"John Boyland. 2001. Alias burying: Unique variables without destructive reads. In S:P&E. 533\u2013553. https:\/\/doi.org\/10.1002\/spe.370 10.1002\/spe.370","DOI":"10.1002\/spe.370"},{"key":"e_1_2_1_15_1","volume-title":"The Dart Programming Language","author":"Bracha Gilad","unstructured":"Gilad Bracha. 2015. The Dart Programming Language. Addison-Wesley. https:\/\/dart.dev"},{"key":"e_1_2_1_16_1","unstructured":"Gilad Bracha. 2017. The Newspeak Language Specification Version 0.1. Feb. https:\/\/newspeaklanguage.org\/"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485523"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3131209"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Nicholas Cameron Sophia Drossopoulou and James Noble. 2013. Understanding Ownership Types with Dependent Types. In Aliasing in Object-Oriented Programming. Types Analysis and Verification. 84\u2013108. https:\/\/doi.org\/10.1007\/978-3-642-36946-9_5 10.1007\/978-3-642-36946-9_5","DOI":"10.1007\/978-3-642-36946-9_5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-024-00738-1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.1998.671113"},{"key":"e_1_2_1_24_1","unstructured":"Christoph Jentsch. 2016. Decentralized Autonomous Organization to automate governance. March https:\/\/download.slock.it\/public\/DAO\/WhitePaper.pdf"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"David G. Clarke John M. Potter and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA. 48\u2013\u00a064. https:\/\/doi.org\/10.1145\/286936.286947 10.1145\/286936.286947","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"David G. Clarke John M. Potter and James Noble. 2001. Simple Ownership Types for Object Containment. In ECOOP. 53\u201376. https:\/\/doi.org\/10.1007\/3-540-45337-7_4 10.1007\/3-540-45337-7_4","DOI":"10.1007\/3-540-45337-7_4"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Ernie Cohen Michal Moskal Wolfram Schulte and Stephan Tobies. 2010. Local Verification of Global Invariants in Concurrent Programs. In CAV. 480\u2013494. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_42 10.1007\/978-3-642-14295-6_42","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"David R. Cok and K. Rustan M. Leino. 2022. Specifying the Boundary Between Unverified and Verified Code. 105\u2013128. https:\/\/doi.org\/10.1007\/978-3-031-08166-8_6 10.1007\/978-3-031-08166-8_6","DOI":"10.1007\/978-3-031-08166-8_6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649835"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304042"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"J. Dedecker T. Van Cutsem S. Mostinckx T. D\u2019Hondt and W. De Meuter. 2006. Ambient-Oriented Programming in AmbientTalk. In ECOOP. 230\u2013254. https:\/\/doi.org\/10.1007\/11785477_16 10.1007\/11785477_16","DOI":"10.1007\/11785477_16"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_1_34_1","volume-title":"Generic Universe Types. In ECOOP (LNCS","volume":"53","author":"Dietl W.","unstructured":"W. Dietl, S. Drossopoulou, and P. M\u00fcller. 2007. Generic Universe Types. In ECOOP (LNCS, Vol. 4609). Springer, 28\u201353. http:\/\/www.springerlink.com"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.9"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Mike Dodds Xinyu Feng Matthew Parkinson and Viktor Vafeiadis. 2009. Deny-guarantee reasoning. In ESOP. 363\u2013377. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_26 10.1007\/978-3-642-00590-9_26","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563298"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"S. Drossopoulou A. Francalanza P. M\u00fcller and A. J. Summers. 2008. A Unified Framework for Verification Techniques for Object Invariants. In ECOOP. 412\u2013437. https:\/\/doi.org\/10.1007\/978-3-540-70592-5_18 10.1007\/978-3-540-70592-5_18","DOI":"10.1007\/978-3-540-70592-5_18"},{"key":"e_1_2_1_41_1","unstructured":"Sophia Drossopoulou Julian Mackay Susan Eisenbach and James Noble. 2025. Reasoning about External Calls \u2013 Extended Version."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Sophia Drossopoulou and James Noble. 2013. The need for capability policies. In FTfJP. 61\u201367. https:\/\/doi.org\/10.1145\/2489804.2489811 10.1145\/2489804.2489811","DOI":"10.1145\/2489804.2489811"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Sophia Drossopoulou James Noble Julian Mackay and Susan Eisenbach. 2020. Holistic Specifications for Robust Programs. In FASE. 420\u2013440. https:\/\/doi.org\/10.1007\/978-3-030-45234-6_21 10.1007\/978-3-030-45234-6_21","DOI":"10.1007\/978-3-030-45234-6_21"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Sophia Drossopoulou James Noble Mark Miller and Toby Murray. 2016. Permission and Authority revisited \u2013 towards a formalization. In (FTfJP). 1 \u2013 6. http:\/\/dl.acm.org\/citation.cfm?id=2955821","DOI":"10.1145\/2955811.2955821"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"J. C Filliatre L. Gondelman and A Pakevichl. 2016. The spirit of ghost code. In Formal Methods System Design. 1\u201316. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_1 10.1007\/978-3-319-08867-9_1","DOI":"10.1007\/978-3-319-08867-9_1"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Robert Bruce Findler and Matthias Felleisen. 2001. Contract Soundness for object-oriented languages. In OOPSLA. 1\u201315. https:\/\/doi.org\/10.1145\/504282.504283 10.1145\/504282.504283","DOI":"10.1145\/504282.504283"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623510"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"Shelly Grossman Ittai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv and Yoni Zohar. 2018. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. POPL https:\/\/doi.org\/10.1145\/3158136 10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Philipp Haller. 2024. Lightweight Affine Types for Safe Concurrency in Scala (Keynote). In Programming. https:\/\/doi.org\/10.1145\/3660829.3661033 https:\/\/speakerdeck.com\/phaller\/towards-safer-lightweight-concurrency-in-scala 10.1145\/3660829.3661033","DOI":"10.1145\/3660829.3661033"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Philipp Haller and Alexander Loiko. 2016. LaCasa: lightweight affinity and object capabilities in Scala. In OOPSLA. 272\u2013291. https:\/\/doi.org\/10.1145\/2983990.2984042 10.1145\/2983990.2984042","DOI":"10.1145\/2983990.2984042"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02928-9_1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_4"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1006\/jvlc.2002.0238"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"S. S. Ishtiaq and P. W. O\u2019Hearn. 2001. BI as an assertion language for mutable data structures. In POPL. 14\u201326. https:\/\/doi.org\/10.1145\/360204.375719 10.1145\/360204.375719","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.13"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_62_1","volume-title":"The Rust Programming Language","author":"Klabnik Steve","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language (2nd ed.). No Starch Press. https:\/\/doc.rust-lang.org\/book\/","edition":"2"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.11.006"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"Dirk Leinenbach and Thomas Santen. 2009. Verifying the Microsoft Hyper-V Hypervisor with VCC. In Formal Methods. 806\u2013809. https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51 10.1007\/978-3-642-05089-3_51","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","unstructured":"K. R. M. Leino and P. M\u00fcller. 2004. Object Invariants in Dynamic Contexts. In ECOOP. 491\u2013516. https:\/\/doi.org\/10.1007\/978-3-540-24851-4_22 10.1007\/978-3-540-24851-4_22","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"e_1_2_1_68_1","unstructured":"Henry M. Levy. 1984. Capability-Based Computer Systems. Butterworth-Heinemann. https:\/\/homes.cs.washington.edu\/~levy\/capabook\/"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591279"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","unstructured":"Anton Lorenzen Stephen Dolan Richard A. Eisenberg and Sam Lindley. 2024. Oxidizing OCaml with Modal Memory Management. In ICFP. 448\u2013475. https:\/\/doi.org\/10.1145\/3674642 10.1145\/3674642","DOI":"10.1145\/3674642"},{"key":"e_1_2_1_72_1","doi-asserted-by":"crossref","unstructured":"Y. Lu and J. Potter. 2006. Protecting Representation with Effect Encapsulation.. In POPL. 359\u2013371. https:\/\/dl.acm.org\/doi\/10.1145\/1111320.1111069 \/10.1145\/1111320.1111069","DOI":"10.1145\/1111037.1111069"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","unstructured":"Matthew Lutze Magnus Madsen Philipp Schuster and Jonathan Immanuel Brachth\u00e4user. 2023. With or Without You: Programming with Effect Exclusion. ICFP 448\u2013475. https:\/\/doi.org\/10.1145\/3607846 10.1145\/3607846","DOI":"10.1145\/3607846"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","unstructured":"Julian Mackay. 2025. Reasoning about External Calls - Coq Model. https:\/\/doi.org\/10.5281\/zenodo.16925157 10.5281\/zenodo.16925157","DOI":"10.5281\/zenodo.16925157"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563317"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","unstructured":"Daniel Marshall and Dominic Orchard. 2024. Functional Ownership through Fractional Uniqueness. In OOPSLA. 1040\u20131070. https:\/\/doi.org\/10.1145\/3649848 10.1145\/3649848","DOI":"10.1145\/3649848"},{"key":"e_1_2_1_77_1","doi-asserted-by":"crossref","unstructured":"Yusuke Matsushita Xavier Denis Jacques-Henri Jourdan and Derek Dreyer. 2022. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In PLDI. ACM 841\u2013856. https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523704 \/10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.20"},{"key":"e_1_2_1_80_1","unstructured":"Adrian Mettler David Wagner and Tyler Close. 2010. Joe-E a Security-Oriented Subset of Java. In NDSS. 357\u2013374. https:\/\/www.ndss-symposium.org\/ndss2010\/joe-e-security-oriented-subset-java"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.5555\/129093"},{"key":"e_1_2_1_83_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation","author":"Miller Mark Samuel","year":"2006","unstructured":"Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Johns Hopkins University, Baltimore, Maryland. https:\/\/papers.agoric.com\/assets\/pdf\/papers\/robust-composition.pdf"},{"key":"e_1_2_1_84_1","unstructured":"Mark Samuel Miller. 2011. Secure Distributed Programming with Object-capabilities in JavaScript. Oct. Talk at Vrije Universiteit Brussel mobicrant-talks.eventbrite.com"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_1"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","unstructured":"Mark Samuel Miller Chip Morningstar and Bill Frantz. 2000. Capability-based Financial Instruments: From Object to Capabilities. In Financial Cryptography. 349\u2013378. https:\/\/doi.org\/10.1007\/3-540-45472-1_24 10.1007\/3-540-45472-1_24","DOI":"10.1007\/3-540-45472-1_24"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","unstructured":"Nick Mitchell. 2006. The Runtime Structure of Object Ownership. In ECOOP. 74\u201398. https:\/\/doi.org\/10.1007\/11785477_5 10.1007\/11785477_5","DOI":"10.1007\/11785477_5"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984021"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_90_1","volume-title":"Analysing the Security Properties of Object-Capability Patterns. Ph. D. Dissertation","author":"Murray Toby","unstructured":"Toby Murray. 2010. Analysing the Security Properties of Object-Capability Patterns. Ph. D. Dissertation. University of Oxford. http:\/\/ora.ox.ac.uk\/objects\/uuid:98b0b6b6-eee1-45d5-b32e-d98d1085c612"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","unstructured":"Takashi Nakayama Yusuke Matsushita Ken Sakayori Ryosuke Sato and Naoki Kobayashi. 2024. Borrowable Fractional Ownership Types for Verification. In VMCAI. 224\u2013246. https:\/\/doi.org\/10.1007\/978-3-031-50521-8_11 10.1007\/978-3-031-50521-8_11","DOI":"10.1007\/978-3-031-50521-8_11"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","unstructured":"James Noble John Potter and Jan Vitek. 1998. Flexible Alias Protection. In ECOOP. 158\u2013185. https:\/\/doi.org\/10.1007\/BFb0054091 10.1007\/BFb0054091","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_94_1","doi-asserted-by":"crossref","unstructured":"Leo Osvald Gr\u00e9gory M. Essertel Xilun Wu Lilliam I. Gonz\u00e1lez Alay\u00f3n and Tiark Rompf. 2016. Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. In OOPSLA. 234\u2013251.","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","unstructured":"M. Parkinson and G. Bierman. 2005. Separation logic and abstraction. In POPL. 247\u2013258. https:\/\/doi.org\/10.1145\/1040305.1040326 10.1145\/1040305.1040326","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASWEC.1998.730915"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","unstructured":"Dustin Rhodes Tim Disney and Cormac Flanagan. 2014. Dynamic Detection of Object Capability Violations Through Model Checking. In DLS. 103\u2013112. https:\/\/doi.org\/10.1145\/2661088.2661099 10.1145\/2661088.2661099","DOI":"10.1145\/2661088.2661099"},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1007\/s42979-019-0012-1"},{"key":"e_1_2_1_103_1","doi-asserted-by":"crossref","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI. 158\u2013174. https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454036 \/10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_30"},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49538-X_15"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919645"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_24"},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2009.8.4.A4"},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49538-X_15"},{"key":"e_1_2_1_112_1","doi-asserted-by":"crossref","unstructured":"Stephan van Staden. 2015. On Rely-Guarantee Reasoning. In MPC. 30\u201349. https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-19797-5_2","DOI":"10.1007\/978-3-319-19797-5_2"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","unstructured":"Guannan Wei Danning Xie Wuqi Zhang Yongwei Yuan and Zhuo Zhang. 2024. Consolidating Smart Contracts with Behavioral Contracts. In PLDI. 965 \u2013 989. https:\/\/doi.org\/10.1145\/3656416 10.1145\/3656416","DOI":"10.1145\/3656416"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1145\/850693.850695"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.15"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","unstructured":"Yichen Xu and Martin Odersky. 2024. A Formal Foundation of Reach Capabilities. In Programming. 134\u2013138. https:\/\/doi.org\/10.1145\/3660829.3660851 10.1145\/3660829.3660851","DOI":"10.1145\/3660829.3660851"},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632927"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763064","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:46:27Z","timestamp":1760031987000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763064"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":118,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763064"],"URL":"https:\/\/doi.org\/10.1145\/3763064","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}