{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:58:26Z","timestamp":1787061506654,"version":"build-2736575974"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Flemish Research Fund"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed---but semantically sound---components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework; to capture termination-insensitivity, we develop a novel language-agnostic theory of Modal Weakest Preconditions. We formalize all of our theory and examples in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3434291","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Mechanized logical relations for termination-insensitive noninterference"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johan","family":"Bay","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159839"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_3_1","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph.D. Dissertation. Princeton University."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341693"},{"key":"e_1_2_1_6_1","volume-title":"Dynamic IFC Theorems for Free! CoRR abs\/","author":"Algehed Maximilian","year":"2005","unstructured":"Maximilian Algehed, Jean-Philippe Bernardy, and Catalin Hritcu. 2020. Dynamic IFC Theorems for Free! CoRR abs\/ 2005.04722 ( 2020 ). arXiv: 2005.04722 https:\/\/arxiv.org\/abs\/ 2005.04722"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139338"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_9_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Log. http:\/\/iris-project. org\/ tutorial-pdfs\/iris-lecture-notes.pdf. ( 2017 )."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_14_1","volume-title":"Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR abs\/","author":"Frumin Dan","year":"1910","unstructured":"Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2019. Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR abs\/ 1910.00905 ( 2019 ). arXiv: 1910.00905 http:\/\/arxiv.org\/abs\/ 1910.00905"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 ( 2018 ) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: a general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017b. Interactive Proofs in Higher-Order Concurrent Separation Logic. In Principles of Programming Languages (POPL).","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676994"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP"},{"key":"e_1_2_1_30_1","volume-title":"Stark","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian D. B. Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 227-273."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351245"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-191382"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784756"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411289"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_4"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Andrei Sabelfeld and David Sands. 2001. A Per Model of Secure Information Flow in Sequential Programs. High. Order Symb. Comput. 14 1 ( 2001 ) 59-91. https:\/\/doi.org\/10.1023\/A:1011553200337 10.1023\/A:1011553200337","DOI":"10.1023\/A:1011553200337"},{"key":"e_1_2_1_39_1","volume-title":"Proc. of the first APPSEM-II workshop, Graham Hutton (Ed.)","author":"Simonet Vincent","year":"2003","unstructured":"Vincent Simonet. 2003a. Flow Caml in a Nutshell. In Proc. of the first APPSEM-II workshop, Graham Hutton (Ed.). Nottingham, United Kingdom."},{"key":"e_1_2_1_40_1","unstructured":"Vincnet Simonet. 2003b. The Flow Caml system. http:\/\/cristal.inria.fr\/~simonet\/soft\/flowcaml"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016868"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290389"},{"key":"e_1_2_1_47_1","unstructured":"Stephan Arthur Zdancewic. 2002. Programming Languages for Information Security. Ph.D. Dissertation. Cornell University USA."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0019-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434291","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434291","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:27:53Z","timestamp":1781854073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434291"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434291"],"URL":"https:\/\/doi.org\/10.1145\/3434291","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}