Yannick Zakowski

Address: Bureau F216, Irisa/Inria
Campus de Beaulieu
263, avenue du général Leclerc
35042 RENNES Cedex - France
Email: yannick.zakowski@irisa.fr

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.

Research Interests

My research interests cover the topics of static analysis of programs, program logics, semantics and proof assistants. I am particularly interested in applying these domains to concurrent programming.



In 2016/2017, I am teaching the following lab sessions:

Various responsabilities

Past research experiences

During my studies, I had the opportunities to do various internships in academia.