一句话：用 classified sets 范畴和 Lawvere 凝聚理论，为模态类型控制信息流建立语义并证明非干涉定理。
论文旨在为“模态类型构造器控制类型间信息流”这一直觉提供严格语义基础。作者研究 classified sets 范畴，它可视为 Abadi 等人提出的信息流指称语义的变体，并证明其为 Lawvere 公理化 cohesion 理论的弱模型。借助这一统一机制，论文对单子式与余单子式模态证明多个 noninterference 定理，并说明 cohesion 如何用于多模态情形下的推理。结论是：cohesion 不仅适用于信息流研究，也为类型论与编程语言中的模态研究提供了有力框架。
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.