Menkar, a proof-assistant for multimodal dependent type theory (MTT), got stuck among other things under the weight of boilerplate code. Allais et al. have developed a very effective generic programming technique for dealing with boilerplate in second-order multisorted algebraic theories (SOMATs) – simple type systems where contexts are lists of types – and Fiore and Szamozvancev provide a categorical/algebraic foundation for this technique. We generalize SOMATs as far as our imagination and the techniques used allow, and propose contextual multisorted algebraic theories (CMATs) as a central concept in a generic programming technique which aims to also support multimodal simple type theory (MSTT), dual-context systems and systems with context exponentiation and an amazing right adjoint.

I am a postdoctoral fellow of the Research Foundation - Flanders (FWO) at imec-DistriNet, KU Leuven, Belgium. I obtained my PhD at this same university in August 2020, and have subsequently worked for 1 year at VUB.

Most of my research is about dependent type theory. There, I am interested in the theory and implementation of modal and presheaf type theory (particularly directed type theory), a quest which also led me to an interest in general syntactic aspects of type theory. I am also fascinated by the question of how to reason about side-effects in dependent type theory. Furthermore, I have been involved in a line of research on categorifying secure compilation.