一句话：提出一种统一的模态结构，用于刻画类型化 λ 演算中的多种模态，并给出其元理论。
本文研究类型化 λ 演算中各种模态（modality）的统一处理，旨在为广泛类型的模态提供通用框架。作者定义了一种一般的模态结构，并论证该结构自然源自直觉主义逻辑的结构，因而能在文献中已有的大量类型系统中找到实例。尽管定义具有较强的一般性，论文仍展示并讨论了该结构丰富的元理论，说明这一统一视角不仅具有概括力，也具备可用的理论性质。论文以理论建构与实例归纳为主，未报告实验评估。
We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.