Abstract
One idiosyncratic framing of type theory is as the study of operations invariant
under substitution. Modal type theory, by contrast, concerns the controlled inte-
gration of operations—modalities—into type theory which violate this discipline,
so-called non-fibered connectives. Modal type theory is therefore built around a
fundamental tension: the desire to include modalities and powerful principles for
reasoning with them on one hand, and the need to maintain the conveniences and
character of Martin-Löf type theory which stem from substitution invariance.
In this thesis we thoroughly explore and discuss this contradiction. We discuss
several different formulations of modal type theory, explore their various syntactic
properties, and relate them through their categorical semantics. In particular, we
show that most modal type theories that have arisen in the last two decades can be
understood through the abstraction of weak dependent right adjoints. We also put
forward a new general modal type theory, MTT, based around this abstraction.
The generality of MTT means that, without any additional work, it can be
specialized to an arbitrary collection of type theories related by modalities and
natural transformations between them. It is therefore easy to obtain a type theory
for a comonad, an adjunction, a local topos, or any other number of complex and
realistic scenarios. In addition to showing that many modal type theories are closely
related to specific instantiations of MTT, we thoroughly explore the syntax and
semantics of MTT itself. We prove that MTT enjoys an unconditional normalization
result and decidable type-checking under mild assumptions. We show how MTT
may be interpreted into a wide variety of structured categories and use this to study
the expressive power of the type theory and various extensions thereof.
Finally, we explore several concrete applications of MTT in the context of
guarded type theory and guarded denotational semantics. We propose a highly usable
language for guarded recursion and explore its particular models and metatheorems.
We show a relatively sharp result bounding the extent to which classical guarded
recursion can be added to any type theory with decidable type-checking and propose
a system to mitigate this issue. Finally, we conduct an in-depth case study using
guarded MTT to obtain a fully synthetic account of the Iris program logic, proving
adequacy in a fully internal manner.
under substitution. Modal type theory, by contrast, concerns the controlled inte-
gration of operations—modalities—into type theory which violate this discipline,
so-called non-fibered connectives. Modal type theory is therefore built around a
fundamental tension: the desire to include modalities and powerful principles for
reasoning with them on one hand, and the need to maintain the conveniences and
character of Martin-Löf type theory which stem from substitution invariance.
In this thesis we thoroughly explore and discuss this contradiction. We discuss
several different formulations of modal type theory, explore their various syntactic
properties, and relate them through their categorical semantics. In particular, we
show that most modal type theories that have arisen in the last two decades can be
understood through the abstraction of weak dependent right adjoints. We also put
forward a new general modal type theory, MTT, based around this abstraction.
The generality of MTT means that, without any additional work, it can be
specialized to an arbitrary collection of type theories related by modalities and
natural transformations between them. It is therefore easy to obtain a type theory
for a comonad, an adjunction, a local topos, or any other number of complex and
realistic scenarios. In addition to showing that many modal type theories are closely
related to specific instantiations of MTT, we thoroughly explore the syntax and
semantics of MTT itself. We prove that MTT enjoys an unconditional normalization
result and decidable type-checking under mild assumptions. We show how MTT
may be interpreted into a wide variety of structured categories and use this to study
the expressive power of the type theory and various extensions thereof.
Finally, we explore several concrete applications of MTT in the context of
guarded type theory and guarded denotational semantics. We propose a highly usable
language for guarded recursion and explore its particular models and metatheorems.
We show a relatively sharp result bounding the extent to which classical guarded
recursion can be added to any type theory with decidable type-checking and propose
a system to mitigate this issue. Finally, we conduct an in-depth case study using
guarded MTT to obtain a fully synthetic account of the Iris program logic, proving
adequacy in a fully internal manner.
| Originalsprog | Engelsk |
|---|
| Forlag | Aarhus University |
|---|---|
| Antal sider | 290 |
| Status | Udgivet - okt. 2023 |