Skip to main content

Daniel Gratzer: Multimodal Dependent Type Theory

Time: Wed 2020-05-27 10.00 - 12.00

Location: Zoom, meeting ID: 610 2070 5696

Participating: Daniel Gratzer, Aarhus University


In this talk, we introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. By varying this mode theory, MTT can be used to reason about a variety of situations, including guarded recursion, axiomatic cohesion, and parametric quantification.

For this talk we focus on two points. First, we introduce the syntax of MTT, and show how the structure of the selected mode theory influences the modalities in the resultant type theory. In doing so we trace through some of the history of modal type theories and show how MTT relates to prior work on dual contexts, left division, and Fitch style modal type theories. Second, we demonstrate how MTT can be applied to one particular modal situation: guarded recursion. In particular, we show how a careful choice of mode theory allows MTT to reason about typical guarded examples. As time permits, we will talk about the impact of these modalities on the glued model of MTT we have used to derive canonicity.

This is joint work with Alex Kavvos, Andreas Nuyts, and Lars Birkedal, and explained in our paper .