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 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).

Recent news

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.


Last update: 2014 07 17