Modalities, Cohesion, and Information Flow

TL;DR

This paper explores how modal type constructors control information flow in programming languages by using the category of classified sets, providing formal noninterference theorems and demonstrating cohesion's role in multi-modal reasoning.

Contribution

It introduces the use of classified sets to rigorously analyze information flow control via modalities and shows how cohesion aids reasoning in multi-modal type systems.

Findings

Proves noninterference theorems for modal constructs

Demonstrates cohesion's utility in multi-modal reasoning

Shows cohesion as a framework for information flow analysis

Abstract

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.