I am currently preparing a PhD thesis on dependently typed programming under Conor McBride's supervision among the MSP group at the University of Strathclyde (Glasgow - Scotland).

Research interests

I am decidedly a type theory enthusiast. Most of my research nowadays revolves around leveraging a type system to enforce invariants, help writing code correct by construction or prevent the user from abusing the interface offered to her. I am passionate about building normalization procedures by exploiting various model construction techniques, developping certified proof search algorithms or constructing universes internalizing desirable properties. My languages of choice are Agda, Haskell and OCaml.

In the past, I have done my fair share of work in Coq (formalizing a good chunk of real analysis dealing with power series) and Isabelle (certifying the output of automated termination tools).

Last update: 2021 11