Projekter pr. år
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.
Originalsprog  Engelsk 

Forlag  ITUniversitetet i København 

Antal sider  99 
ISBN (Trykt)  9788779493896 
Status  Udgivet  2022 
Navn  ITUDS 

Nummer  193 
ISSN  16023536 
Fingeraftryk
Dyk ned i forskningsemnerne om 'Cubical modal type theories'. Sammen danner de et unikt fingeraftryk.Projekter
 1 Afsluttet

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
Projekter: Projekt › Forskning