{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:32:05Z","timestamp":1784845925451,"version":"3.55.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["H98230-23-C-0275"],"award-info":[{"award-number":["H98230-23-C-0275"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1901033"],"award-info":[{"award-number":["CCF-1901033"]}],"id":[{"id":"10.13039\/100000001","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":[[2026,1,8]]},"abstract":"<jats:p>\n                    Substructural type systems provide the ability to speak about\n                    <jats:italic toggle=\"yes\">resources<\/jats:italic>\n                    . By enforcing usage restrictions on\n                    <jats:italic toggle=\"yes\">inputs<\/jats:italic>\n                    to computations they allow programmers to reify limited system units\u2013such as memory\u2013in types. We demonstrate a new form of resource reasoning founded on constraining\n                    <jats:italic toggle=\"yes\">outputs<\/jats:italic>\n                    and explore its utility for practical programming. In particular, we identify a number of disparate programming features explored largely in the security literature as various fragments of our unified framework. These encompass capabilities, quantitative information leakage, sandboxing in the style of the Linux\n                    <jats:monospace>seccomp<\/jats:monospace>\n                    interface, authorization protocols, and more. We furthermore explore its connection to conventional input-based resource reasoning, casting it as an internal treatment of the constructive Kripke semantics of substructural logics. We verify the\n                    <jats:italic toggle=\"yes\">capability, quantity,<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">protocol<\/jats:italic>\n                    safety of our system through a single logical relations argument. In doing so, we take the first steps towards obtaining the ultimate multitool for security reasoning.\n                  <\/jats:p>","DOI":"10.1145\/3776669","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"777-805","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Security Reasoning via Substructural Dependency Tracking"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3888-8440","authenticated-orcid":false,"given":"Hemant","family":"Gouni","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8279-5817","authenticated-orcid":false,"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","volume-title":"Entailment, Vol. II: The Logic of Relevance and Necessity","author":"Anderson Alan R.","year":"1992","unstructured":"Alan R. Anderson et al.. 1992. Entailment, Vol. II: The Logic of Relevance and Necessity. Princeton University Press."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2018. \u201cSyntax and Semantics of Quantitative Type Theory.\u201d In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201918) 56\u201365. doi:10.1145\/3209108.3209189.","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Nick Benton and Philip Wadler. 1996. \u201cLinear Logic Monads and the Lambda Calculus.\u201d In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS \u201996) 420. doi:10.1109\/LICS.1996.561458.","DOI":"10.1109\/LICS.1996.561458"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Nils Anders Danielsson. 2008. \u201cLightweight semiformal time complexity analysis for purely functional data structures.\u201d In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201908) 133\u2013144. doi:10.1145\/1328438.1328457.","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_7_1","volume-title":"Cryptography and data security","author":"Denning Dorothy E.","year":"1982","unstructured":"Dorothy E. Denning. 1982. Cryptography and data security. Addison-Wesley."},{"key":"e_1_3_2_8_1","volume-title":"Ph.D. Dissertation","author":"Dolan Stephen","year":"2016","unstructured":"Stephen Dolan. 2016. \u201cAlgebraic subtyping.\u201d Ph.D. Dissertation. University of Cambridge."},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Soichiro Fujii Shin-ya Katsumata and Paul-Andr\u00e9 Melli\u00e8s. 2016. \u201cTowards a Formal Theory of Graded Monads.\u201d In: Foundations of Software Science and Computation Structures 513\u2013530. doi:10.1007\/978-3-662-49630-5_30.","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Marco Gaboardi Shin-ya Katsumata Dominic Orchard Flavien Breuvart and Tarmo Uustalu. 2016. \u201cCombining effects and coeffects via grading.\u201d In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016) 476\u2013489. doi:10.1145\/2951913.2951939.","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Deepak Garg and Frank Pfenn. 2006. \u201cNon-Interference in Constructive Authorization Logic.\u201d In: Proceedings of the 19th IEEE Workshop on Computer Security Foundations (CSFW \u201906) 283\u2013296. doi:10.1109\/CSFW.2006.18.","DOI":"10.1109\/CSFW.2006.18"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Dan R. Ghica and Alex I. Smith. 2014. \u201cBounded Linear Types in a Resource Semiring.\u201d In: Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410 331\u2013350. doi:10.1007\/978-3-642-54833-8_18.","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3764116"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17772505"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.mcm.2013.02.006"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2025.15"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019915908844"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Max Kanovich Stepan Kuznetsov Vivek Nigam and Andre Scedrov. 2018. A Logical Framework with Commutative and Non-commutative Subexponentials. In: Automated Reasoning 228\u2013245. doi:10.1007\/978-3-319-94205-6_16.","DOI":"10.1007\/978-3-319-94205-6_16"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000117"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata. 2014. \u201cParametric effect monads and semantics of effect systems.\u201d In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914) 633\u2013645. doi:10.1145\/2535838.2535846.","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Eric Koskinen and Tachio Terauchi. 2014. \u201cLocal temporal reasoning.\u201d In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS \u201914) Article 59 10 pages. doi:10.1145\/2603088.2603138.","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Paul Blain Levy. 1999. \u201cCall-by-Push-Value: A Subsuming Paradigm.\u201d In: Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA \u201999) 228\u2013242. doi:10.1007\/3-540-48959-2_17.","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/356678.356682"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649848"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Dylan McDermott and Tarmo Uustalu. 2022. \u201cFlexibly Graded Monads and Graded Algebras.\u201d In: Mathematics of Program Construction: 14th International Conference (MPC 2022) 102\u2013128. doi:10.1007\/978-3-031-16912-0_4.","DOI":"10.1007\/978-3-031-16912-0_4"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Benjamin Moon Harley Eades III and Dominic Orchard. 2021. \u201cGraded Modal Dependent Type Theory.\u201d In: Programming Languages and Systems 462\u2013490. doi:10.1007\/978-3-030-72019-3_17.","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Jamie Morgenstern Deepak Garg and Frank Pfenning. 2011. \u201cA Proof-Carrying File System with Revocable and Use-Once Certificates.\u201d In: Security and Trust Management - 7th International Workshop (STM 2011) Revised Selected Papers (Lecture Notes in Computer Science). Vol. 7170 40\u201355. doi:10.1007\/978-3-642-29963-6_5.","DOI":"10.1007\/978-3-642-29963-6_5"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Dominic Orchard Philip Wadler and Harley Eades III. 2020. \u201cUnifying graded and parameterised monads.\u201d In: Eighth Workshop on Mathematically Structured Functional Programming (MSFP). doi:https:\/\/doi.org\/10.4204\/EPTCS.317.2 10.4204\/EPTCS.317.2.","DOI":"10.4204\/EPTCS.317.2"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Dominic Orchard and Nobuko Yoshida. 2016. Effects as sessions sessions as effects. Principles of Programming Languages 568\u2013581. doi:10.1145\/2837614.2837634.","DOI":"10.1145\/2837614.2837634"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Tomas Petricek Dominic Orchard and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. International Conference on Functional Programming 123\u2013135. doi:10.1145\/2628136.2628160.","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_2_37_1","unstructured":"Frank Pfenning. 2023. \u201cLecture Notes on Resource Semantics.\u201d https:\/\/www.cs.cmu.edu\/~fp\/courses\/15836-f23\/lectures\/19-resource.pdf."},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin and John Power. 2001. \u201cAdequacy for Algebraic Effects.\u201d In: Foundations of Software Science and Computation Structures 1\u201324. doi:10.1007\/3-540-45315-6_1.","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/2214699"},{"key":"e_1_3_2_40_1","unstructured":"Klaas Pruiksma William Chargin Frank Pfenning and Jason Reed. 2018. \u201cAdjoint logic.\u201d Unpublished manuscript. https:\/\/www.cs.cmu.edu\/~fp\/papers\/adjoint18b.pdf."},{"key":"e_1_3_2_41_1","volume-title":"Ph.D. Dissertation","author":"Reed Jason","year":"2009","unstructured":"Jason Reed. 2009. \u201cA hybrid logical framework.\u201d Ph.D. Dissertation. Carnegie Mellon University."},{"key":"e_1_3_2_42_1","article-title":"Focus-preserving embeddings of substructural logics in intuitionistic logic.","author":"Reed Jason","year":"2010","unstructured":"Jason Reed and Frank Pfenning. 2010. Focus-preserving embeddings of substructural logics in intuitionistic logic. Unpublished manuscript. https:\/\/www.cs.cmu.edu\/~fp\/papers\/substruct10.pdf.","journal-title":"Unpublished manuscript"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Jason Reed and Benjamin C. Pierce. 2010. \u201cDistance makes the types grow stronger: a calculus for differential privacy.\u201d In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201910) 157\u2013168. doi:10.1145\/1863543.1863568.","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_44_1","unstructured":"Sophia Roshal and Frank Pfenning. 2025. Unpublished communications. https:\/\/www.cs.cmu.edu\/~fp\/courses\/15417-s25\/lectures\/18-adjord.pdf."},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Christian Skalka and Scott Smith. 2004. \u201cHistory Effects and Verification.\u201d In: Programming Languages and Systems 107\u2013128. doi:10.1007\/978-3-540-30477-7_8.","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Geoffrey Smith. 2009. \u201cOn the Foundations of Quantitative Information Flow.\u201d In: Foundations of Software Science and Computational Structures 288\u2013302. doi:10.1007\/978-3-642-00596-1_21.","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1981.1675753"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543920"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Luis Caires and Frank Pfenning. 2012. \u201cFunctions as Session-Typed Processes.\u201d In: Foundations of Software Science and Computational Structures 346\u2013360. doi:10.1007\/978-3-642-28729-9_23.","DOI":"10.1007\/978-3-642-28729-9_23"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:45:26Z","timestamp":1784209526000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776669"],"URL":"https:\/\/doi.org\/10.1145\/3776669","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}