{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T21:13:19Z","timestamp":1764364399708,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modalities of a monadic and comonadic flavour. The common machinery behind our theorems stems from the the fact that classified sets are a (weak) model of Lawvere's theory of axiomatic cohesion. In the process, we show how cohesion can be used for reasoning about multi-modal settings. This leads to the conclusion that cohesion is a particularly useful setting for the study of both information flow, but also modalities in type theory and programming languages at large.<\/jats:p>","DOI":"10.1145\/3290333","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Modalities, cohesion, and information flow"],"prefix":"10.1145","volume":"3","author":[{"given":"G. A.","family":"Kavvos","sequence":"first","affiliation":[{"name":"Wesleyan University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"volume-title":"New Structures for Physics","author":"Abramsky Samson","key":"e_1_2_1_2_1"},{"volume-title":"Category Theory","author":"Awodey Steve","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"volume-title":"Handbook of Categorical Algebra","author":"Borceux Francis","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"volume-title":"Applications of Categories in Computer Science","author":"Brookes Stephen","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"The guarded lambda calculus: Programming and reasoning with guarded recursion for coinductive types","volume":"12","author":"Clouston Ranald","year":"2016","journal-title":"Logical Methods in Computer Science"},{"volume-title":"Categories for Types","author":"Crole Roy L.","key":"e_1_2_1_9_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172707"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237788"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"volume-title":"Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy. IEEE, 11\u201311","author":"Goguen J. A.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"e_1_2_1_18_1","unstructured":"Martin Hofmann. 1999. Type Systems for Polynomial-Time Computation. Habilitation thesis. Technischen Universit\u00e4t Darmstadt. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/99\/ECS- LFCS- 99- 406\/  Martin Hofmann. 1999. Type Systems for Polynomial-Time Computation. Habilitation thesis. Technischen Universit\u00e4t Darmstadt. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/99\/ECS- LFCS- 99- 406\/"},{"volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"Johnstone Peter T.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500588"},{"key":"e_1_2_1_23_1","first-page":"2","article-title":"Secure Computer Systems: Mathematical Foundations","volume":"4","author":"LaPadula Leonard J.","year":"1996","journal-title":"Journal of Computer Security"},{"key":"e_1_2_1_24_1","first-page":"41","article-title":"Axiomatic cohesion","volume":"19","author":"Lawvere F. William","year":"2007","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_1_25_1","first-page":"909","article-title":"Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness","volume":"30","author":"William Lawvere F.","year":"2015","journal-title":"Theory and Applications of Categories"},{"volume-title":"Proceedings of LFCS","year":"2016","author":"Daniel","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","volume-title":"2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Dale Miller (Ed.)","volume":"84","author":"Licata Daniel R.","year":"2017"},{"volume-title":"Categories for the Working Mathematician. Graduate Texts in Mathematics","author":"Lane Saunders Mac","key":"e_1_2_1_28_1"},{"volume-title":"Proceedings of the Workshop on Foundations of Computer Security (FCS\u201904)","year":"2004","author":"Miyamoto Kenji","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"volume-title":"Types for Information Flow Control: Labeling Granularity and Semantic Models. In 31st IEEE Symposium on Computer Security Foundations (CSF 2018","year":"2018","author":"Rajani Vineet","key":"e_1_2_1_36_1"},{"volume-title":"Computer Science Laboratory, SRI","year":"1986","author":"Rushby John","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011553200337"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:10)2008"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Thomas Streicher. 2006. Domain-theoretic Foundations of Functional Programming. World Scientific.   Thomas Streicher. 2006. Domain-theoretic Foundations of Functional Programming. World Scientific.","DOI":"10.1142\/6284"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016868"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.029"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290333","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290333"],"URL":"https:\/\/doi.org\/10.1145\/3290333","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}