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).
I am interested in logic (constructivist) and its relation to computations. It obviously involve pieces of type theory for its logical and computational aspects. I enjoy working on a blackboard as much as using a programming language with dependent types (such as Agda) or a proof assistant (such as Coq).
2013/04: Submission to ICFP of a paper written with Conor and Pierre Boutillier !
2012/12: My first year report on normalization by evaluation for simply-typed lambda calculi equipped with primitives on datatypes is now available.
