Projects per year
Abstract
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 noninterference guarantees.
The thesis contains two papers. The first paper presents a type theory with a family of Fitchstyle 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 nondeterministic 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 2category 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 2category.
The thesis contains two papers. The first paper presents a type theory with a family of Fitchstyle 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 nondeterministic 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 2category 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 2category.
Original language  English 

Publisher  ITUniversitetet i København 

Number of pages  99 
ISBN (Print)  9788779493896 
Publication status  Published  2022 
Series  ITUDS 

Number  193 
ISSN  16023536 
Fingerprint
Dive into the research topics of 'Cubical modal type theories'. Together they form a unique fingerprint.Projects
 1 Finished

Type theories for reactive programming
Møgelberg, R. E. (PI), Vezzosi, A. (CoI), Graulund, C. U. (CoI), Kristensen, M. B. (CoI) & Veltri, N. (CoI)
22/01/2016 → 21/01/2022
Project: Research