{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:11Z","timestamp":1750219991807,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"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":[[2023,1,9]]},"abstract":"<jats:p>\n            This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon (some five years after the publication of his celebrated quantitative theory of communication), describes how the information content of channels can be described\n            <jats:italic>qualitatively<\/jats:italic>\n            , but still abstractly, in terms of\n            <jats:italic>information elements<\/jats:italic>\n            , where information elements can be viewed as equivalence relations over the data source domain. Shannon showed that these elements have a partial ordering, expressing when one information element is more informative than another, and that these partially ordered information elements form a complete lattice. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for understanding and reasoning about information flow.\n          <\/jats:p>\n          <jats:p>The second theory of information is Dana Scott\u2019s domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott\u2019s partial ordering also represents when one element is more informative than another, but in the sense of computational progress \u2013 i.e. when one element is a more defined or evolved version of another.<\/jats:p>\n          <jats:p>\n            To give a satisfactory account of information flow in computer programs it is necessary to consider both theories together, in order to understand not only what information is conveyed by a program (viewed as a channel, \u00e0 la Shannon) but also how the precision with which that information can be observed is determined by the definedness of its encoding (\u00e0 la Scott). To this end we show how these theories can be fruitfully combined, by defining\n            <jats:italic>the Lattice of Computable Information<\/jats:italic>\n            (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon\u2019s theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott\u2019s ordering captures possible varieties in the way that information is presented.\n          <\/jats:p>\n          <jats:p>We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses.<\/jats:p>","DOI":"10.1145\/3571740","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1987-2016","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Reconciling Shannon and Scott with a Lattice of Computable Information"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7255-4465","authenticated-orcid":false,"given":"Sebastian","family":"Hunt","sequence":"first","affiliation":[{"name":"City University of London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6221-0503","authenticated-orcid":false,"given":"David","family":"Sands","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5608-8273","authenticated-orcid":false,"given":"Sandro","family":"Stucki","sequence":"additional","affiliation":[{"name":"Amazon Prime Video, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"volume-title":"Proc. ACM Symp. on Principles of Programming Languages. 147\u2013160","author":"Abadi M.","unstructured":"M. Abadi , A. Banerjee , N. Heintze , and J. Riecke . 1999. A Core calculus of Dependency . In Proc. ACM Symp. on Principles of Programming Languages. 147\u2013160 . M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. 1999. A Core calculus of Dependency. In Proc. ACM Symp. on Principles of Programming Languages. 147\u2013160.","key":"e_1_2_1_1_1"},{"volume-title":"Fifth Annual IEEE Symposium on Logic in Computer Science, 355\u2013365","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi and Gordon D. Plotkin . 1990. A PER model of polymorphism and recursive types. [1990] Proceedings . Fifth Annual IEEE Symposium on Logic in Computer Science, 355\u2013365 . Mart\u00edn Abadi and Gordon D. Plotkin. 1990. A PER model of polymorphism and recursive types. [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, 355\u2013365.","key":"e_1_2_1_2_1"},{"volume-title":"Domain Theory and the Logic of Observable Properties. Ph. D. Dissertation","author":"Abramsky Samson","unstructured":"Samson Abramsky . 1987. Domain Theory and the Logic of Observable Properties. Ph. D. Dissertation . University of London. Samson Abramsky. 1987. Domain Theory and the Logic of Observable Properties. Ph. D. Dissertation. University of London.","key":"e_1_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1016\/0168-0072(91)90065-T"},{"volume-title":"Information, processes and games. J. Benthem van & P","author":"Abramsky Samson","unstructured":"Samson Abramsky . 2008. Information, processes and games. J. Benthem van & P . Adriaans (Eds.), Philosophy of Information , 483\u2013549. Samson Abramsky. 2008. Information, processes and games. J. Benthem van & P. Adriaans (Eds.), Philosophy of Information, 483\u2013549.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","volume-title":"Handbook of Logic in Computer Science (Vol. 3): Semantic Structures","author":"Abramsky Samson","year":"1985","unstructured":"Samson Abramsky and Achim Jung . 1995. Domain Theory . In Handbook of Logic in Computer Science (Vol. 3): Semantic Structures . Oxford University Press, Inc. , USA. 1\u2013168. isbn:0 1985 3762X Samson Abramsky and Achim Jung. 1995. Domain Theory. In Handbook of Logic in Computer Science (Vol. 3): Semantic Structures. Oxford University Press, Inc., USA. 1\u2013168. isbn:019853762X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1007\/978-3-319-96131-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/CSF.2012.31"},{"volume-title":"Proc. European Symp. on Research in Computer Security.","author":"Askarov A.","unstructured":"A. Askarov , S. Hunt , A. Sabelfeld , and D. Sands . 2008. Termination Insensitive noninterference leaks more than just a bit . In Proc. European Symp. on Research in Computer Security. A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. 2008. Termination Insensitive noninterference leaks more than just a bit. In Proc. European Symp. on Research in Computer Security.","key":"e_1_2_1_9_1"},{"volume-title":"Proc. IEEE Symp. on Security and Privacy. 207\u2013221","author":"Askarov A.","unstructured":"A. Askarov and A. Sabelfeld . 2007. Gradual Release: Unifying Declassification, Encryption and Key Release Policies . In Proc. IEEE Symp. on Security and Privacy. 207\u2013221 . A. Askarov and A. Sabelfeld. 2007. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In Proc. IEEE Symp. on Security and Privacy. 207\u2013221.","key":"e_1_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/CSF.2009.22"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1109\/CSF49147.2020.00015"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/2784731.2784733"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.5555\/2595038.2595040"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/1067625.806556"},{"unstructured":"M. Coppo and M. Zacchi. 1986. Type inference and logical relations. In LICS. \t\t\t\t  M. Coppo and M. Zacchi. 1986. Type inference and logical relations. In LICS.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/360051.360056"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1145\/359636.359712"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1111\/j.1749-6632.1993.tb52513.x"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/964001.964017"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/3175660"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/3434291"},{"volume-title":"Abstract interpretation of functional languages: from theory to practice. Ph. D. Dissertation","author":"Hunt Sebastian","unstructured":"Sebastian Hunt . 1991. Abstract interpretation of functional languages: from theory to practice. Ph. D. Dissertation . Imperial College London , UK. Sebastian Hunt. 1991. Abstract interpretation of functional languages: from theory to practice. Ph. D. Dissertation. Imperial College London, UK.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","volume-title":"The PER Model of Abstract Non-interference","author":"Hunt Sebastian","year":"1971","unstructured":"Sebastian Hunt and Isabella Mastroeni . 2005. The PER Model of Abstract Non-interference . In Static Analysis, Chris Hankin and Igor Siveroni (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 171\u2013185. isbn:978-3-540-3 1971 -9 Sebastian Hunt and Isabella Mastroeni. 2005. The PER Model of Abstract Non-interference. In Static Analysis, Chris Hankin and Igor Siveroni (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 171\u2013185. isbn:978-3-540-31971-9"},{"key":"e_1_2_1_25_1","volume-title":"Binding Time Analysis: A New PERspective. In In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201991","author":"Hunt Sebastian","year":"1991","unstructured":"Sebastian Hunt and David Sands . 1991 . Binding Time Analysis: A New PERspective. In In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201991 . ACM Press, 154\u2013164. Sebastian Hunt and David Sands. 1991. Binding Time Analysis: A New PERspective. In In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201991. ACM Press, 154\u2013164."},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1109\/CSF51468.2021.00031"},{"volume-title":"6th IEEE Computer Security Foundations Workshop - CSFW\u201993","author":"Landauer J.","unstructured":"J. Landauer and T. Redmond . 1993. A Lattice of Information . In 6th IEEE Computer Security Foundations Workshop - CSFW\u201993 , Proceedings. IEEE Computer Society, 65\u201370. J. Landauer and T. Redmond. 1993. A Lattice of Information. In 6th IEEE Computer Security Foundations Workshop - CSFW\u201993, Proceedings. IEEE Computer Society, 65\u201370.","key":"e_1_2_1_27_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.3390\/e13030683"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/1040305.1040319"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1017\/S0960129513000649"},{"volume-title":"Principles of Security and Trust, Mart\u00edn Abadi and Steve Kremer (Eds.)","author":"McIver Annabelle","unstructured":"Annabelle McIver , Carroll Morgan , Geoffrey Smith , Barbara Espinoza , and Larissa Meinicke . 2014. Abstract Channels and Their Robust Information-Leakage Ordering . In Principles of Security and Trust, Mart\u00edn Abadi and Steve Kremer (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg . 83\u2013102. isbn:978-3-642-54792-8 Annabelle McIver, Carroll Morgan, Geoffrey Smith, Barbara Espinoza, and Larissa Meinicke. 2014. Abstract Channels and Their Robust Information-Leakage Ordering. In Principles of Security and Trust, Mart\u00edn Abadi and Steve Kremer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 83\u2013102. isbn:978-3-642-54792-8","key":"e_1_2_1_31_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1109\/RISP.1994.296590"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1145\/2676726.2676970"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1215\/S0012-7094-42-00942-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1137\/0205035"},{"key":"e_1_2_1_36_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress.","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types , Abstraction and Parametric Polymorphism. In IFIP Congress. John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress."},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/978-0-387-21798-7_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"unstructured":"Olivier Rioul Julien B\u00e9guinot Victor Rabiet and Antoine Souloumiac. 2022. La v\u00e9ritable (et m\u00e9connue) th\u00e9orie de l\u2019information de Shannon. In 28e Colloque GRETSI\u201922. \t\t\t\t  Olivier Rioul Julien B\u00e9guinot Victor Rabiet and Antoine Souloumiac. 2022. La v\u00e9ritable (et m\u00e9connue) th\u00e9orie de l\u2019information de Shannon. In 28e Colloque GRETSI\u201922.","key":"e_1_2_1_39_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1023\/A:1011553200337","article-title":"A Per Model of Secure Information Flow in Sequential Programs","volume":"14","author":"Sabelfeld A.","year":"2001","unstructured":"A. Sabelfeld and D. Sands . 2001 . A Per Model of Secure Information Flow in Sequential Programs . Journal of Higher-Order and Symbolic Computation , 14 , 1 (2001), March , 59 \u2013 91 . A. Sabelfeld and D. Sands. 2001. A Per Model of Secure Information Flow in Sequential Programs. Journal of Higher-Order and Symbolic Computation, 14, 1 (2001), March, 59\u201391.","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.3233\/JCS-2009-0352"},{"key":"e_1_2_1_43_1","volume-title":"A mathematical theory of communication. The Bell system technical journal, 27, 3","author":"Shannon C.","year":"1948","unstructured":"C. Shannon . 1948. A mathematical theory of communication. The Bell system technical journal, 27, 3 ( 1948 ), 379\u2013423. C. Shannon. 1948. A mathematical theory of communication. The Bell system technical journal, 27, 3 (1948), 379\u2013423."},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1109\/TIT.1953.1188572"},{"volume-title":"Power domains and predicate transformers: A topological view","author":"Smyth M. B.","unstructured":"M. B. Smyth . 1983. Power domains and predicate transformers: A topological view . In Automata, Languages and Programming, Josep Diaz (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 662\u2013675. isbn:978-3-540-40038-7 M. B. Smyth. 1983. Power domains and predicate transformers: A topological view. In Automata, Languages and Programming, Josep Diaz (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 662\u2013675. isbn:978-3-540-40038-7","key":"e_1_2_1_45_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1145\/3474834"},{"volume-title":"FSCD, the 7th International Conference on Formal Structures for Computation and Deduction.","author":"Sterling Jonathan","unstructured":"Jonathan Sterling and Robert Harper . 2022. Sheaf semantics of termination-insensitive noninterference . In FSCD, the 7th International Conference on Formal Structures for Computation and Deduction. Jonathan Sterling and Robert Harper. 2022. Sheaf semantics of termination-insensitive noninterference. In FSCD, the 7th International Conference on Formal Structures for Computation and Deduction.","key":"e_1_2_1_47_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1145\/1016848.1016868"},{"volume-title":"Topology via Logic","author":"Vickers Steven","unstructured":"Steven Vickers . 1989. Topology via Logic . Cambridge University Press , USA. isbn:0521360625 Steven Vickers. 1989. Topology via Logic. Cambridge University Press, USA. isbn:0521360625","key":"e_1_2_1_49_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.5555\/353629.353648"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571740","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571740","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:33Z","timestamp":1750182573000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571740"],"URL":"https:\/\/doi.org\/10.1145\/3571740","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}