Contributions to Multimode and Presheaf Type Theory

Dependent type theory is a powerful logic for both secure programming and computer assisted proving about programs. Dependently typed languages such as Agda, Coq and Idris can therefore be used both as programming languages and as proof assistants. The goal of this PhD project is to establish directed dependent type theories (DDTT) by formulating them, implementing them, proving their consistency and demonstrating their use. By a DDTT, we mean a dependent type theory which has not only a built-in notion of equality, but also of structure preserving transformation. By including the notion of structure preservation in the foundations of the system, rather than defining it on an ad-hoc basis as is done in classical mathematics, we expect to obtain many theorems (including all parametricity theorems) and even some operations for free. For example, when we define a functorial type former, such as List, we expect its functorial action (fmap) to be implemented automatically. This is especially useful when reasoning about or programming with more complicated concepts, such as monad transformations, which implement the effects of one monad in terms of another, or transformations between mathematical structures. DDTT will also give us a better understanding of subtyping in the context of dependent types. This is of particular interest for the programming language Scala, which has subtyping at its core and was recently extended with some basic support for dependent types.status: publishe