{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:53Z","timestamp":1784200253297,"version":"3.55.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000005","name":"DOD 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":"NSF","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":[[2025,10,9]]},"abstract":"<jats:p>\n                    Information flow control is a long-studied approach for establishing\n                    <jats:italic toggle=\"yes\">non-interference<\/jats:italic>\n                    properties of programs. For instance, it can be used to prove that a secret does not interfere with some computation, thereby establishing that the former does not leak through the latter. Despite their potential as a holy grail for security reasoning and their maturity within the literature, information flow type systems have seen limited adoption. In practice, information flow specifications tend to be excessively complex and can easily spiral out of control even for simple programs. Additionally, while non-interference is well-behaved in an idealized setting where information leakage never occurs, most practical programs\n                    <jats:italic toggle=\"yes\">must<\/jats:italic>\n                    violate non-interference in order to fulfill their purpose. Useful information flow type systems in prior work must therefore contend with a definition of non-interference extended with\n                    <jats:italic toggle=\"yes\">declassification,<\/jats:italic>\n                    which often offers weaker modular reasoning properties.\n                  <\/jats:p>\n                  <jats:p>\n                    We introduce\n                    <jats:italic toggle=\"yes\">structural information flow,<\/jats:italic>\n                    which both illuminates and addresses these issues from a logical viewpoint. In particular, we draw on established insights from the modal logic literature to argue that information flow reasoning arises from\n                    <jats:italic toggle=\"yes\">hybrid logic,<\/jats:italic>\n                    rather than conventional modal logic as previously imagined. We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a\n                    <jats:italic toggle=\"yes\">natural<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">unavoidable<\/jats:italic>\n                    consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.\n                  <\/jats:p>","DOI":"10.1145\/3764116","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3954-3980","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Structural Information Flow: A Fresh Look at Types for Non-interference"],"prefix":"10.1145","volume":"9","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":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Martin Abadi Anindya Banerjee Nevin Heintze Jon G. Riecke . 1999. A core calculus of dependency. In:Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery POPL '99 San Antonio Texas USA 147-160.doi:10.1145\/292540.292555","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Aslan Askarov Sebastian Hunt Andrei Sabelfeld David Sands . 2008. Termination-insensitive noninterference leaks more than just a bit. Computer Security-ESORICS 2008: 13th European Symposium on Research in Computer Security. Springer Malaga Spain October 6-8 2008 333-348.doi: 10.1007\/978-3-540-88313-5_22","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Pritam Choudhury Harley Eades III Stephanie Weirich . 2022. A Dependent Dependency Calculus. European Symposium on Programming. Springer International Publishing Cham 403-430.doi:10.1007\/978-3-030-99336-8_15","DOI":"10.1007\/978-3-030-99336-8_15"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Raimil Cruz Eric Tanter . 2019. Existential Types for Relaxed Noninterference. Programming Languages and Systems. Springer International Publishing Cham 73-92.doi:10.1007\/978-3-030-34175-6_5","DOI":"10.1007\/978-3-030-34175-6_5"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/3180976"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers Lars Birkedal . 2021. Compositional Non-Interference for Fine-Grained Concurrent Programs. 2021 IEEE Symposium on Security and Privacy (SP). 1416-1433.doi:10.1109\/SP40001.2021.00003","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/64805"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Joseph A Goguen Jose Meseguer . 1982. Security policies and security models. 1982 IEEE Symposium on Security and Privacy. IEEE 11-11.doi:10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17013074"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1410234.1410239"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata . 2014. Parametric effect monads and semantics of effect systems. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery 633-645.doi:10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1561\/3300000008"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Paul Blain Levy . 1999. Call-by-push-value: A subsuming paradigm. International Conference on Typed Lambda Calculi and Applications. Springer 228-243.doi:10.1007\/3-540-48959-2_17","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632886"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"John C. Mitchell Gordon D. Plotkin . 1985. Abstract types have existential types. Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Association for Computing Machinery 37-51.doi:10.1145\/318593.318606","DOI":"10.1145\/318593.318606"},{"key":"e_1_3_1_22_2","unstructured":"Kenji Miyamoto Atsushi Igarashi . 2004. A modal foundation for secure information flow. Workshop on Foundations of Computer Security. 187-203."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"E. Moggi . 1989. Computational lambda-calculus and monads. Fourth Annual Symposium on Logic in Computer Science. 14-23.doi:10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_1_24_2","unstructured":"Andrew C Myers . 1999. Mostly-static decentralized information flow control. Massachusetts Institute of Technology.doi:1721.1\/16717"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1048512"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Minh Ngo David A Naumann Tamara Rezk . 2020. Type-Based Declassification for Free. Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods. Springer 181-197.doi:10.1007\/978-3-030-63406-3_11","DOI":"10.1007\/978-3-030-63406-3_11"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632890"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Francois Pottier Vincent Simonet . 2002. Information flow inference for ML. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery 319-330.doi:10.1145\/503272.503302","DOI":"10.1145\/503272.503302"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.2307\/2214699"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Vineet Rajani Deepak Garg . 2018. Types for Information Flow Control: Labeling Granularity and Semantic Models. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 233-246.doi:10.1109\/CSF.2018.00024","DOI":"10.1109\/CSF.2018.00024"},{"key":"e_1_3_1_35_2","volume-title":"A hybrid logical framework","author":"Reed Jason","year":"2009","unstructured":"Jason Reed . 2009. A hybrid logical framework. Carnegie Mellon University."},{"key":"e_1_3_1_36_2","unstructured":"John C. Reynolds . 1984. Types Abstraction and Parametric Polymorphism. Information Processing 83: Proceedings of the IFIP 9th World Computer Congress. Elsevier Science Publishers B. V. (North-Holland) Amsterdam 513-523."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0352"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_24"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling Robert Harper . 2022. Sheaf Semantics of Termination-Insensitive Noninterference. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl - Leibniz-Zentrum fur Informatik 5:1-5:19.doi:10.4230\/LIPIcs.FSCD.2022.5","DOI":"10.4230\/LIPIcs.FSCD.2022.5"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000313106"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Stephen Tse Steve Zdancewic . 2004. Translating dependency into parametricity. Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming. Association for Computing Machinery 115-125.doi:10.1145\/1016850.1016868","DOI":"10.1145\/1016850.1016868"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764116","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:14:34Z","timestamp":1784196874000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":40,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3764116"],"URL":"https:\/\/doi.org\/10.1145\/3764116","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","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"}}]}}