Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 16:05 - 16:27 at Sala I - Security and Information Flow Chair(s): David Walker

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

15:21 - 16:27: Research Papers - Security and Information Flow at Sala I
Chair(s): David WalkerPrinceton University
POPL-2019-Research-Papers15:21 - 15:43
James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park
Link to publication DOI File Attached
POPL-2019-Research-Papers15:43 - 16:05
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 File Attached
POPL-2019-Research-Papers16:05 - 16:27
G. A. KavvosWesleyan University
Link to publication DOI Pre-print File Attached