Address: Bureau F216, Irisa/Inria
Campus de Beaulieu
263, avenue du général Leclerc
35042 RENNES Cedex - France
I am currently a PhD student in the Celtique team under the supervision of David Pichardie and David Cachera . We are overall notably interested in the formalization in the Coq proof assistant of realistic compilers for realistic languages.
My current primary line of work is to investigate the gap which separates us from the verified compilation of a high-level concurrent language. This led me so far to conduct two major projects with the collaboration of my co-authors. First, to formalise and prove correct an on-the-fly garbage collector in the Coq proof assistant. The algorithm is programmed in a dedicated intermediate representation, and proved using a sound rely-guarantee-based proof system. Second to investigate the refinement of concurrent linearizable objects. Most specifically, we derive observational refinements through the use of rely/guarantee Hoare-style logics, allowing us to compile our intermediate representation down to a lower-level language.
A curriculum vitae may be found here.