Modal Type Theory (2015)
(Valéria de Paiva, Nuance Communications, US)
Type theory does not usually discuss logical modalities, and modalities tend to be mostly studied within classical logic, not type theory. But modalities should be useful in type theory, as they are generally very useful in theoretical computer science.
Since there seems to be a renewed interest in the notions of constructive modal type theory and linear type theory, in part caused by the interest in homotopy type theory, it seems sensible to recapitulate some of the known facts, especially ones on the semantics of modal type theory. I will describe a fibrational categorical semantics for the necessity-only fragment of constructive modal type theory, both with and without dependent types.
Dependent type theories are usually, but not always, given categorical semantics in terms of fibrations. We provide semantics in terms of fibrations for both the non-dependent and the dependent modal type systems proposed and prove them sound and complete. We also discuss some of the possible alternatives.
(This is joint work with Eike Ritter, Birmingham)
Click for slides.
Since there seems to be a renewed interest in the notions of constructive modal type theory and linear type theory, in part caused by the interest in homotopy type theory, it seems sensible to recapitulate some of the known facts, especially ones on the semantics of modal type theory. I will describe a fibrational categorical semantics for the necessity-only fragment of constructive modal type theory, both with and without dependent types.
Dependent type theories are usually, but not always, given categorical semantics in terms of fibrations. We provide semantics in terms of fibrations for both the non-dependent and the dependent modal type systems proposed and prove them sound and complete. We also discuss some of the possible alternatives.
(This is joint work with Eike Ritter, Birmingham)
Click for slides.
