Publications

Drafts

• A concurrency model based on monadic interpreters: Executable semantics for a concurrent subset of LLVM IR
  Nicolas Chappe, Ludovic Henrio and Yannick Zakowski
  [draft, repo]
• An abstract, certified account of operational game semantics
  Peio Borthelle, Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski
  [draft, repo]

International Conferences

• A Two-Phase Infinite/Finite Low-Level Memory Model
  Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski and Steve Zdancewic
  Accepted for publication at ICFP'24.
  [(non definitive) paper, repo]

• Abstract Interpreters: a Monadic Approach to Modular Verification
  Sébastien Michelland, Laure Gonnord and Yannick Zakowski
  Accepted for publication at ICFP'24.
  [(non definitive) paper, repo]

• Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
  Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski and Steve Zdancewic
  Accepted for publication at POPL'23.
  [paper, slides, repo]

• Formal Reasoning About Layered Monadic Interpreters
  Irene Yoon, Yannick Zakowski and Steve Zdancewic
  Accepted for publication at ICFP'22.
  [paper, doc, repo]

• Modular, Compositional, and Executable Formal Semantics for LLVM IR
  Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva and Steve Zdancewic
  Accepted for publication at ICFP'21.
  [paper, slides, repo]

• An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
  Paul He, Chung-kil Hur, Yannick Zakowski and Steve Zdancewic
  Accepted for publication at CPP'20.
  [paper, slides, integrated in paco]

• Interaction Trees -- Representing Recursive and Impure Programs in Coq
  Li-yao Xia, Yannick Zakowski, Paul He, Chung-kil Hur, Gregory Malecha, Benjamin Pierce and 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, slides, 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]

Others

• Toward Sustainable Conferences: an Analysis of SIGLPAN Registration Data
  Cristina C. Lopes, Benjamin Pierce and Yannick Zakowski
  [draft, repo]