Modal Type Theory as a Library with Applications in Effect Parametricity

Many variants of type theory extend a base theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs that would be harder or impossible to do in the base theory. However, implementing such extended type theories (either from scratch or by modifying an existing implementation) is a big hurdle for their wider adoption. In this PhD project I am developing Sikkel, a library in the dependently typed programming language Agda that allows users to program in extended type theories. At a later stage, I will study and develop effect parametricity (parametric quantification over a monad) as a tool for reasoning about effects and the authority to perform effects (capabilities). This will be possible by using an extended dependent type theory with primitives for parametricity, implemented in the Sikkel library.