I am interested in concrete denotational semantics
for lambda-calculi and their interactions. More precisely I am working on:
Models of pure lambda-calculus: used for studying the lattice of lambda-theories, in particular its interactions with computability theory.
Quantitative semantics: building parametrised concrete semantics either to extract quantitative information or to model resource sensitive calculi.
Probabilistic (higher order) Rewriting: Understanding probabilistic reduction and termination.
By transitivity I am also interested in many related domains: logic, algebra, proof theory, computability theory, complexity theory, language design, circuit design, cryptography protocols (differential privacy)...