{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:16Z","timestamp":1781855596943,"version":"3.54.5"},"reference-count":54,"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\/100014037","name":"National Defense Science and Engineering Graduate","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100014037","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":[[2021,1,4]]},"abstract":"<jats:p>\n                    Type systems designed for information-flow control commonly use a\n                    <jats:italic toggle=\"yes\">program-counter label<\/jats:italic>\n                    to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation.\n                  <\/jats:p>","DOI":"10.1145\/3434316","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":3,"title":["Giving semantics to program-counter labels via secure effects"],"prefix":"10.1145","volume":"5","author":[{"given":"Andrew K.","family":"Hirsch","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ethan","family":"Cecchetti","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"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","unstructured":"Mart\u00edn Abadi Anindya Banerjee Nevin Heintze and Jon Riecke. 1999. A Core Calculus of Dependency. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/292540.292555 10.1145\/292540.292555","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341693"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Maximilian Algehed and Alejandro Russo. 2017. Encoding DCC in Haskell. In Programming Languages and Analysis for Security (PLAS). https:\/\/doi.org\/10.1145\/3139337.3139338 10.1145\/3139337.3139338","DOI":"10.1145\/3139337.3139338"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Owen Arden. 2017. Flow-Limited Authorization. Ph.D. Dissertation. Cornell University. https:\/\/doi.org\/10.7298\/X4HX19P9 10.7298\/X4HX19P9","DOI":"10.7298\/X4HX19P9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52592-0_60"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Soichiro Fujii Shin-ya Katsumata and Paul-Andr\u00e9 Mellis\u00e8s. 2016. Towards a Formal Theory of Graded Monads. In Foundations of Software Science and Computational Structures (FOSSACS). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_30 10.1007\/978-3-662-49630-5_30","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"e_1_2_1_13_1","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"Galatos Nikolaos","year":"2007","unstructured":"Nikolaos Galatos. 2007. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier Sience."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_16_1","volume-title":"Hirsch and Ethan Cecchetti","author":"Andrew","year":"2020","unstructured":"Andrew K. Hirsch and Ethan Cecchetti. 2020. Giving Semantics to Program-Counter Labels via Secure Efects. Technical Report. Max Planck Institute for Software Systems. https:\/\/arxiv.org\/abs\/ 2010.13191"},{"key":"e_1_2_1_17_1","unstructured":"Alan Jefrey. 1997. Premonoidal Categoies and a Graphical View of Programs. http:\/\/fpl.cs.depaul.edu\/ajefrey\/premon\/ paper.html"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata. 2014. Parametric Efect Monads and Semantics of Efect Systems. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2535838.2535846 10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"G. A. Kavvos. 2019. Modalities Cohesion and Information Flow. In Principles of Programming Languages (POPL). https: \/\/doi.org\/10.1145\/3290333 10.1145\/3290333","DOI":"10.1145\/3290333"},{"key":"e_1_2_1_20_1","volume-title":"International Cryptology Conference (CRYPTO). Springer, 104-113","author":"Kocher Paul C","year":"1996","unstructured":"Paul C Kocher. 1996. Timing attacks on implementations of Difie-Hellman, RSA, DSS, and other systems. In International Cryptology Conference (CRYPTO). Springer, 104-113."},{"key":"e_1_2_1_21_1","unstructured":"Daan Leijen. 2016. Type Directed Compilation of Row-Typed Algebraic Efects. Technical Report. Microsoft. https:\/\/www. microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/08\/algef-tr-2016-1.pdf"},{"key":"e_1_2_1_22_1","volume-title":"Myers","author":"Liu Jed","year":"2017","unstructured":"Jed Liu, Owen Arden, Michael D. George, and Andrew C. Myers. 2017. Fabric: Building Open Distributed Systems Securely by Construction. Journal of Computer Security (JCS) 25 ( 2017 ). https:\/\/doi.org\/10.323\/JCS-15805 10.323\/JCS-15805"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"J. M. Lucassen and D. K. Giford. 1988. Polymorphic Efect Systems. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/73560.73564 10.1145\/73560.73564","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_24_1","volume-title":"Myers","author":"Magrino Tom","year":"2016","unstructured":"Tom Magrino, Jed Liu, Owen Arden, Chinawat Isradisaikul, and Andrew C. Myers. 2016. Jif 3.5: Java Information Flow. ( June 2016 ). https:\/\/www.cs.cornell.edu\/jif Software release."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Daniel Marino and Todd Milstein. 2009. A Generic Type-and-Efect System. In Types in Language Design and Implementation (TLDI). https:\/\/doi.org\/10.1145\/1481861.1481868 10.1145\/1481861.1481868","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192375"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93 1 ( 1991 ). https:\/\/doi.org\/10. 1016\/ 0890-5401 ( 91 ) 90052-4 10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382289"},{"key":"e_1_2_1_30_1","first-page":"228","article-title":"JFlow: Practical mostly-static information flow control","author":"Myers Andrew C.","year":"1999","unstructured":"Andrew C. Myers. 1999. JFlow: Practical mostly-static information flow control. In Principles of Programming Languages (POPL). 228-241.","journal-title":"Principles of Programming Languages (POPL)."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Flemming Nielson. 1996. Annotated Type and Efect Systems. ACM Computing Surveys (CSUR) 28 2 ( 1996 ). https: \/\/doi.org\/10.1145\/234528.234745 10.1145\/234528.234745","DOI":"10.1145\/234528.234745"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_6"},{"key":"e_1_2_1_33_1","unstructured":"Dominic Orchard Tomas Petricek and Alan Mycroft. 2014. The Semantic Marriage of Efects and Monads. ( 2014 ). https: \/\/arxiv.org\/abs\/1401.5391"},{"key":"e_1_2_1_34_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C","unstructured":"Benjamin C Pierce. 2002. Types and Programming Languages. MIT press."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin and John Power. 2003. Algebraic Operations and Generic Efects. Applied Categorical Structures 11 1 ( 2003 ). https:\/\/doi.org\/10.1023\/A:1023064908962 10.1023\/A:1023064908962","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Fran\u00b8ois Pottier and Vincent Simonet. 2002. Information Flow Inference for ML. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/503272.503302 10.1145\/503272.503302","DOI":"10.1145\/503272.503302"},{"key":"e_1_2_1_38_1","unstructured":"Matija Pretnar. 2010. The Logic and Handling of Algebraic Efects. Ph.D. Dissertation. School of Informatics The University of Edinburgh. http:\/\/hdl.handle.net\/ 1842 \/4611"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411289"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Andrei Sabelfeld and David Sands. 2001. A PER Model of Secure Information Flow in Sequential Programs. Higher-Order and Symbolic Computation 14 1 ( 2001 ). https:\/\/doi.org\/10.1023\/A:1011553200337 10.1023\/A:1011553200337","DOI":"10.1023\/A:1011553200337"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4("},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Ross Tate. 2013. The Sequential Semantics of Producer Efect Systems. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2429069.2429074 10.1145\/2429069.2429074","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016868"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1997.596807"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289429"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","unstructured":"Lucas Waye Pablo Buiras Dan King Stephen Chong and Alejandro Russo. 2015. It's My Privilege: Controlling Downgrading in DC-Labels. In Security and Trust Management (STM). https:\/\/doi.org\/10.1007\/978-3-319-24858-5_13 10.1007\/978-3-319-24858-5_13","DOI":"10.1007\/978-3-319-24858-5_13"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020843229247"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434316","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434316","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:24:42Z","timestamp":1781853882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434316"],"URL":"https:\/\/doi.org\/10.1145\/3434316","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"}}]}}