Abstract
Modalities provide powerful abstractions for various problems of mathematics and computer science.
For example, they find applications in staged programming, program security properties, reactive programming, concurrency and step-indexing.
Type theory combines logic and programming in one language.
This allows us to write and reason about programs in type theory, as well as to interpret other programming languages.
The goal of this thesis is twofold: On one hand, we explore applications of a specific modal type theory, namely guarded type theory, in programming language semantics.
On the other hand, we describe how a general framework for modal type theories can be turned into a proof assistant.
We show how to use a constructive guarded type theory to reason about FPC, a programming language with recursive types, and probabilistic FPC, which extends FPC by probabilistic choice.
We define both operational and denotational semantics for FPC as well as its probabilistic extension and prove soundness.
By doing this, we provide the first semantics of probabilistic FPC in constructive type theory.
Finally, we construct a relation between syntax and semantics and show how to prove contextual equivalence between programs.
It is difficult to reason about languages with recursion and computational effects such as probabilistic choice, because these features have no obvious counterpart in type theory.
By using the later modality of guarded type theory and a special guarded fixpoint combinator, it is possible to define semantic domains that interpret these effects.
Using modalities to abstract low-level details away significantly simplifies the task at hand for practitioners.
To truly benefit from these capabilities, a proof assistant that automates simpler arguments and validates the correctness of complicated proofs is of the essence.
However, implementing a proof assistant is a difficult undertaking and unfortunately, many modalities cannot be handled by current proof assistants.
Furthermore, we explain how to implement the general modal type theory MTT, which can internalize many different modal situations.
Importantly, this includes a guarded type theory comparable to the one used for the interpretation of probabilistic FPC.
However, the framework is general enough to internalize arbitrary collections of (dependent) right adjoints.
The resulting proof assistant "mitten" is modular and specializes to many modal situation.
For example, they find applications in staged programming, program security properties, reactive programming, concurrency and step-indexing.
Type theory combines logic and programming in one language.
This allows us to write and reason about programs in type theory, as well as to interpret other programming languages.
The goal of this thesis is twofold: On one hand, we explore applications of a specific modal type theory, namely guarded type theory, in programming language semantics.
On the other hand, we describe how a general framework for modal type theories can be turned into a proof assistant.
We show how to use a constructive guarded type theory to reason about FPC, a programming language with recursive types, and probabilistic FPC, which extends FPC by probabilistic choice.
We define both operational and denotational semantics for FPC as well as its probabilistic extension and prove soundness.
By doing this, we provide the first semantics of probabilistic FPC in constructive type theory.
Finally, we construct a relation between syntax and semantics and show how to prove contextual equivalence between programs.
It is difficult to reason about languages with recursion and computational effects such as probabilistic choice, because these features have no obvious counterpart in type theory.
By using the later modality of guarded type theory and a special guarded fixpoint combinator, it is possible to define semantic domains that interpret these effects.
Using modalities to abstract low-level details away significantly simplifies the task at hand for practitioners.
To truly benefit from these capabilities, a proof assistant that automates simpler arguments and validates the correctness of complicated proofs is of the essence.
However, implementing a proof assistant is a difficult undertaking and unfortunately, many modalities cannot be handled by current proof assistants.
Furthermore, we explain how to implement the general modal type theory MTT, which can internalize many different modal situations.
Importantly, this includes a guarded type theory comparable to the one used for the interpretation of probabilistic FPC.
However, the framework is general enough to internalize arbitrary collections of (dependent) right adjoints.
The resulting proof assistant "mitten" is modular and specializes to many modal situation.
| Original language | English |
|---|---|
| Qualification | PhD |
| Awarding Institution |
|
| Supervisors/Advisors |
|
| Award date | 15 Aug 2024 |
| Place of Publication | Aarhus |
| Publisher | |
| Publication status | Published - 15 Aug 2024 |