Programming language semantics in modal type theories

TY - GEN

T1 - Programming language semantics in modal type theories

AU - Stassen, Philipp Jan Andries

N1 - Published 2024

PY - 2024/8/15

Y1 - 2024/8/15

N2 - 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.

AB - 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.

M3 - PhD thesis

T3 - PhD Theses - Department of Computer Science

PB - Department of Computer Science, University of Aarhus

CY - Aarhus

ER -