Constructive Modalities
Topos Institute
Abstract:
Modalities (temporal, epistemic, deontic, etc) have proved themselves extremely useful in theoretical computer science, multi-agent systems and AI, usually in the setting of classical logic. Recently there seems to be a renewed interest in the notions of *constructive* (or intuitionistic) modal type theory and linear type theory, in part because of the interest in homotopy type theory. Since I have been working on modal extensions of the Curry-Howard correspondence to logical systems since the 90s, it seems a good idea to recap some of the old ideas associated with modal type theory. Especially because it seems to me that there are plenty of old problems that have not been solved, yet.