Publications

Drafts

• Choice Trees: Representing and Reasoning About Nondeterministic, Recursive, and Impure Programs in Rocq
  Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski and Steve Zdancewic
  Under revision at Journal of Functional Programming (JFP).
  [draft]

International Conferences

• An abstract, certified account of operational game semantics
  Peio Borthelle, Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski
  Accepted for publication at ESOP'25.
  [paper, extended version, repo, artifact report]

• A concurrency model based on monadic interpreters: Executable semantics for a concurrent subset of LLVM IR
  Nicolas Chappe, Ludovic Henrio and Yannick Zakowski
  Accepted for publication at CPP'25.
  [paper, repo]

• 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.
  [paper, repo]

• Abstract Interpreters: a Monadic Approach to Modular Verification
  Sébastien Michelland, Laure Gonnord and Yannick Zakowski
  Accepted for publication at ICFP'24.
  [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 (November 2019), repo]