Programming language semantics in modal type theories

Modalities provide powerful abstractions for various problems of mathematics and computer science.<br/> For example, they find applications in staged programming, program security properties, reactive programming, concurrency and step-indexing.<br/><br/> Type theory combines logic and programming in one language.<br/> This allows us to write and reason about programs in type theory, as well as to interpret other programming languages.<br/><br/> 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. <br/> On the other hand, we describe how a general framework for modal type theories can be turned into a proof assistant. <br/><br/> 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. <br/> We define both operational and denotational semantics for FPC as well as its probabilistic extension and prove soundness.<br/> By doing this, we provide the first semantics of probabilistic FPC in constructive type theory.<br/> Finally, we construct a relation between syntax and semantics and show how to prove contextual equivalence between programs.<br/> 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.<br/> 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.<br/><br/> Using modalities to abstract low-level details away significantly simplifies the task at hand for practitioners. <br/> To truly benefit from these capabilities, a proof assistant that automates simpler arguments and validates the correctness of complicated proofs is of the essence.<br/> However, implementing a proof assistant is a difficult undertaking and unfortunately, many modalities cannot be handled by current proof assistants. <br/><br/> Furthermore, we explain how to implement the general modal type theory MTT, which can internalize many different modal situations. <br/> Importantly, this includes a guarded type theory comparable to the one used for the interpretation of probabilistic FPC. <br/> However, the framework is general enough to internalize arbitrary collections of (dependent) right adjoints.<br/> The resulting proof assistant "mitten" is modular and specializes to many modal situation.