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.
Modalities, Cohesion, and Information Flow (POPL slides) (popl19-clsfds.pdf) | 5.49MiB |
Fri 18 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
15:21 - 16:27: Security and Information FlowResearch Papers at Sala I Chair(s): David WalkerPrinceton University | |||
15:21 - 15:43 Talk | LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park Link to publication DOI Media Attached File Attached | ||
15:43 - 16:05 Talk | From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers Marco VassenaChalmers University of Technology, Alejandro RussoChalmers University of Technology, Sweden, Deepak GargMax Planck Institute for Software Systems, Vineet RajaniMPI-SWS, Deian StefanUniversity of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 - 16:27 Talk | Modalities, Cohesion, and Information Flow Research Papers Alex KavvosWesleyan University Link to publication DOI Pre-print File Attached |