Modalities, Cohesion, and Information Flow
This work addresses foundational issues in programming language theory for researchers and practitioners interested in type systems and information security, but it is incremental as it builds on existing semantics and cohesion theory.
The paper tackles the problem of rigorously understanding how modal type constructors control information flow in programming calculi by studying the category of classified sets, a denotational semantics variant, and proves multiple noninterference theorems for monadic and comonadic modalities. The result shows that cohesion provides a useful framework for reasoning about information flow and modalities in type theory and programming languages.
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.