Preoccupation
I am interested in (Martin Löf’s) type theory, dependent types, intuitionistic mathematics in general, category theory, and functional programming. I am particularly interested in the type theoretic semantics of catgory theory and of type theory itself, and the category theoretic semantics of type theory.