Modalities, cohesion, and information flow

G. A. Kavvos*

*Corresponding author for this work

Research output: Contribution to journalArticle (Academic Journal)

19 Downloads (Pure)

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.
Original languageEnglish
Article number20
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume3
Issue numberPOPL
DOIs
Publication statusPublished - 2 Jan 2019
Event46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) - Hotel Cascais Miragem, Cascais, Portugal
Duration: 13 Jan 201919 Jan 2019
Conference number: 2019
https://popl19.sigplan.org/

Bibliographical note

Provisional acceptance date added, based on publication information

Structured keywords

  • Programming Languages

Keywords

  • information flow
  • information flow control
  • type systems
  • modal type systems
  • cohesion
  • modal type theory
  • modalities
  • noninterference
  • category theory

Fingerprint Dive into the research topics of 'Modalities, cohesion, and information flow'. Together they form a unique fingerprint.

Cite this