A unified view of modalities in type systems
Andreas M. Abel, Jean-Philippe Bernardy · Proceedings of the ACM on Programming Languages · 2020
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.