| 2026 | CPP | Layers of Confluence for Actors. | Ludovic Henrio, Einar Broch Johnsen, smund Aqissiaq Arild Klvstad, Violet Ka I Pun, Yannick Zakowski |
| 2025 | CPP | Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR. | Nicolas Chappe, Ludovic Henrio, Yannick Zakowski |
| 2025 | ESOP | An abstract, certified account of operational game semantics. | Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski |
| 2025 | ESOP | Artifact Report: an Abstract, Certified Account of Operational Game Semantics. | Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski |
| 2020 | CPP | An equational theory for weak bisimulation via generalized parameterized coinduction. | Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic |
| 2018 | SAC | Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. | Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie |
| 2017 | ITP | Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |