I am a postdoctoral researcher under Laura Kovács in the FORSYTE group of informatics department of TU Wien in Vienna, Austria. My main research interests lie in type theory, its applications to proof assistants, automated theorem proving, its applications to blockchain protocols, and logic.
One way of studying compatibility of type theories is by looking at their transformations. To accommodate for the use in proof assistants, the transformations we consider are syntactic in nature, they preserve derivability and are general enough to be applicable to a large class of type theories. The transformations preserve some syntactic structure (like judgement kinds and syntactic classes) and they interact nicely with substitutions of variables and instantiations of metavariables: with the action on expressions they form a relative monad for syntax.