Se interesa en teoría de tipos dependientes, especialmente
TT de Martin-Löf, y en semántica de lenguajes de programación.
En particular, ha estado estudiando Normalización por Evaluación
(NbE) para teorías de tipos. Su objetivo actual es desarrollar
la teoría necesaria para implementar un lenguaje con tipos dependientes
basado en NbE.