Cubical modal type theories

The goal of this thesis is to combine Cubical Type Theory (CTT) and modal type theory towards obtaining a type theory suitable for the verification of programs relying on features such as recursion. For this purpose the main advantage of CTT is that extensionality principles such as function extensionality can be shown as theorems, and as such can be given computational content. Additionally CTT supports the powerful univalence axiom as well as the highly useful Higher Inductive Types (HITs). Another extension to type theory is that of modalities which can be used to encode the primitives needed for programming with and reasoning about recursion, staged computation, and information flow control. Combining these two approaches offers the promise of a type theory with the necessary amount of structure to encode e.g., reactive programs with productivity guarantees and programs relying on control of information flow between types with non-interference guarantees.
The thesis contains two papers. The first paper presents a type theory with a family of Fitch-style later modalities indexed over an object of clocks, called Clocked Cubical Type Theory (CCTT). Guarded recursion with multiple clocks has been used in earlier work to encode coinductive types. The primary novelty in this theory is induction under clocks for HITs. The encoding of coinductive types requires functors which commute with clock quantification and a large class of these can be produced by applying induction under clocks. One example of interest is the finite powerset functor, which allows for the encoding of non-deterministic processes. The theory is shown to be sound by the construction of a presheaf model.
In the second paper a more general framework called Cubical Modal Type Theory is presented. This extends the existing framework of Multimodal Type Theory (MTT) with the primitives of CTT. MTT is a modal type theory indexed by a 2-category of modes which is flexible enough to encode S4, cohesive type theory, and guarded recursion. Cubical Modal Type Theory extends this theory with the computationally well understood path types. The primary contribution of the paper is a method for the quick production of models in the style of Orton and Pitts. One of the technical challenges in achieving this is the construction of composition structures on modal types, which requires the cubical structure to be coherent with respect to the indexing 2-category.