During my PhD studies, I investigated how modal type theories can be used to study other programming languages. Type theories are special programming languages which also function as mathematical logic and are thus well suited to reason about programs. Modal type theories (such as guarded type theories) then allow us to consider more complicated programming languages.
To truly benefit from the expressiveness of modal type theories, a proof assistant that automates simpler arguments and validates the correctness of complicated proofs is of the essence. Therefore, I also investigated how to implement a proof assistant for different modal type theories.
The results of this thesis are twofold: I contribute to the study of programming languages in constructive guarded type theory, and furthermore give the algorithms which are needed to implement a multimodal proof assistant.
I completed my PhD study at the Department of Computer Science, Faculty of Natural Sciences, Aarhus University.