Mike Shulman has started a discussion on modal type theory. Here are a few things in this direction – more will likely follow.
Please add relevant references below. Selected references to the (very large) CS literature would be welcome.
The following was the proceedings of a meeting some years ago in Trieste. My paper was concerned with the modality that can be used to interprete
the calculus of constructions logic in the propositions as types logic.
Mathematical Structures in Computer Science
Volume 11, Number 4, August 2001: Modalities in Type Theory
Matt Fairtlough, Michael Mendler, Eugenio Moggi: Special issue: Modalities in type theory. 507-509
Frank Pfenning, Rowan Davies: A judgmental reconstruction of modal logic. 511-540
Peter Aczel: The Russell-Prawitz modality. 541-554
Joëlle Despeyroux, Pierre Leleu: Recursion over objects of functional type. 555-572
Jacob M. Howe: Proof search in Lax Logic. 573-588
Mauro Ferrari, Camillo Fiorentini, Pierangelo Miglioli: Extracting information from intermediate semiconstructive HA-systems - extended abstract. 589-596The work on monadic semantics of computation and effect-type systems is closely related to modal type theory.
Moggi’s original work introduced the idea that different notions of computation correspond to different (strong) monads:
Among the huge follow-up literature, Andrzej Filinski’s work tackles the question of how to navigate between different notions of computation, applying an idea he terms monadic reflection together with an effect type system:
A more concrete illustration of these ideas is present in
where the authors describe how to use monadic reflection to embed a modality of probabilistic computations within a functional language.