News
About
Since October 2020, I am a researcher at Inria as a member of the CASH research group, hosted in the LIP research laboratory at ENS Lyon.
I am broadly interested in the formal verification of software, and have put so far through my work a particular emphasis on verified compilation. I formalize most of my work in the Coq proof assistant.
Currently, I notably work on the vellvm project, a formalization in the Coq proof assistant of LLVM's infrastructure, and LLVM IR's semantics in particular. This led me to work on the representation of effectful programs in type theory, as well as new techniques to conduct coinductive reasoning. An account for the application of these techniques to model LLVM IR can be found in here.
Before joining Inria, I was a postdoctoral researcher at the University of Pennsylvania, in the programming language research group, working with Steve Zdancewic as part of the DeepSpec NSF Expedition. I still actively collaborate with Steve and other collaborators from Philadelphia, most notably as part of the Vellvm project.
Previously, I was a doctoral researcher in France in the Celtique team under the supervision of David Pichardie and David Cachera. I worked during this time on the formal verification of an on-the-fly concurrent garbage collector in the Coq proof assistant.
On a different note, I am extremely concerned by and interested in finding solutions for the need for all activities, and hence research in particular, to strive for carbon neutrality. I have worked with Crista Lopez and Benjamin Pierce as part of the SIGPLAN and climate change initiative. I have written a tool to estimate a conference's footprint and understand its source. I have co-authored a report (in progress) about the application of this tool to the major SIGPLAN conferences.
A curriculum vitae may be found here.
Publications
International Conferences
- Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
Accepted for publication at POPL'23.. [paper, repo]
- Formal Reasoning About Layered Monadic Interpreters
Irene Yoon, Yannick Zakowski, Steve Zdancewic
Accepted for publication at ICFP'22. [paper , proof, repo]
- Modular, Compositional, and Executable Formal Semantics for LLVM IR
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
Accepted for publication at ICFP'21. [paper, repo]
- An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Paul He, Chung-kil Hur, Yannick Zakowski, Steve Zdancewic
Accepted for publication at CPP'20. [paper]
- Interaction Trees -- Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He, Chung-kil Hur, Gregory Malecha, Benjamin Pierce, Steve Zdancewic
Accepted for publication at POPL'20. [paper, repo]
- Compilation of Linearizable Data Structures: A Mechanised RG Logic for Semantic Refinement
Yannick Zakowski, David Cachera, Delphine Demange and David Pichardie.
In the 33rd ASM/SIGAPP Symposium on Applied Computing (SAC'18).
[paper, slides, doi, companion website]
- Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan and Jan Vitek.
In Interactive Theorem Proving (ITP'17)
[paper, slides, doi, companion website]
Workshops
- Effectful programming across heterogeneous computations
Jean Abou Samra , Martin Bodin and Yannick Zakowski
In Journées Francophones des Langages Applicatifs (JFLA'23)
[paper, repo]
- Games and Strategies using Coinductive Types
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski
In International Conference on Types for Proofs and Programs (TYPES'23)
[abstract, slides , talk]
- (Co)datatypes via W-setoids and M-setoids
Galaad Langlois, Damien Pous and Yannick Zakowski
In The Coq Workshop 2023
[abstract, slides]
Journals
- Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology (extended journal version)
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan and Jan Vitek.
In Journal of Automated Reasoning (JAR'19)
[paper, doi]
Thesis
- Verification of a Concurrent Garbage Collector
Yannick Zakowski
Doctoral Thesis, ENS de Rennes, 2017
[manuscript]
Drafts
- Abstract Interpreters: a Monadic Approach to Modular Verification
Sébastien Michelland, Laure Gonnord, Yannick Zakowski
Under Submission [draft, repo]
- Toward Sustainable Conferences: an Analysis of SIGLPAN Registration Data
Cristina C. Lopes, Benjamin Pierce and Yannick Zakowski
[draft, repo]
Advising
Current students
- Nicolas Chappe (PhD student, co-advised with Matthieu Moy)
- Peio Borthelle (PhD student, co-advised with Tom Hirschowitz and Guilhem Jaber)
Teaching
2021/2023
- Static Analysis for Optimizing Compilers, with Christophe Alias and Laure Gonnord (ENS Lyon, M2)
- Program verification with coinduction and proof assistants, with Damien Pous (ENS Lyon, M2)
2020/2021
-
Contribution to the compilation course "CAP" at ENS Lyon.
Service
- Program commitee: CPP'21, JFLA'21, ICFP'22
- I co-organized in 2016 the first edition of the french national seminary for PhD students in computer science: SDOC
- External reviewer (CPP'20,TACAS16,JFLA15,LMCS14)
- Student volunteer at the European Conference on Object-Oriented Programming 2015 (ECOOP'15) in Prague
Past research experiences
During my studies, I had the opportunities to do various internships in academia.- I spent four months in Göteborg, Sweden, with Dave Sands, working on Information Flow Control and more precisely the Paragon compiler. A report may be found here.
- I investigated with David Cachera numerical methods to infer polynomial inequalities as program invariants. A report may be found here.
- I did a ten-months internship at the Aarhus University, in the Logics and Semantics group, under the supervision of Lars Birkedal and Filip Sieczkowski . I notably worked with Filip to build semantic models and formalize their correctness in Coq using his recently designed library for solving recursive domain equations. This line of work notably led to the ModuRes tutorial. Two reports can be found respectively here and there.