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 JanDisplayed time zone: Belfast change
15:21 - 16:27 | |||
15:21 22mTalk | LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park Link to publication DOI Media Attached File Attached | ||
15:43 22mTalk | From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 22mTalk | Modalities, Cohesion, and Information Flow Research Papers Alex Kavvos Wesleyan University Link to publication DOI Pre-print File Attached |