Tail Modulo Async-Await Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
Under submission.
[draft]
International Conferences and Journals
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
Accepted for publication in Journal of Functional Programming (JFP)---2025. Note: this journal publication essentially extends and superseeds its preceeding POPL homonymous.
[paper]
[repo]
Structural Temporal Logic for Mechanized Program Verification
Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel
Accepted for publication at ECOOP'25.
[paper,
repo]
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]
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]
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]