Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (ITP, 2017)

Verification of a Concurrent Garbage Collector. (Vérification d'un glaneur de cellules concurrent). - Yannick Zakowski (2017)

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. - Yannick Zakowski; David Cachera; Delphine Demange; David Pichardie (SAC, 2018)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (J. Autom. Reason., 2019)

An equational theory for weak bisimulation via generalized parameterized coinduction. - Yannick Zakowski; Paul He; Chung-Kil Hur; Steve Zdancewic (CPP, 2020)

Interaction trees: representing recursive and impure programs in Coq. - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2020)

Modular, compositional, and executable formal semantics for LLVM IR. - Yannick Zakowski; Calvin Beck; Irene Yoon 001; Ilia Zaichuk; Vadim Zaliva; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Formal reasoning about layered monadic interpreters. - Irene Yoon 001; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2022)

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. - Nicolas Chappe; Paul He; Ludovic Henrio; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2023)

A Two-Phase Infinite/Finite Low-Level Memory Model. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (CoRR, 2024)

Structural temporal logic for mechanized program verification. - Eleftherios Ioannidis; Yannick Zakowski; Steve Zdancewic; Sebastian Angel (CoRR, 2024)

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2024)

Abstract Interpreters: A Monadic Approach to Modular Verification. - Sébastien Michelland; Yannick Zakowski; Laure Gonnord (Proc. ACM Program. Lang., 2024)

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR. - Nicolas Chappe; Ludovic Henrio; Yannick Zakowski (CPP, 2025)

An abstract, certified account of operational game semantics. - Peio Borthelle; Tom Hirschowitz; Guilhem Jaber; Yannick Zakowski (ESOP (1), 2025)

Artifact Report: an Abstract, Certified Account of Operational Game Semantics. - Peio Borthelle; Tom Hirschowitz; Guilhem Jaber; Yannick Zakowski (ESOP (1), 2025)

Front Matter, Table of Contents, Preface, Conference Organization. - Karine Even-Mendoza; Raphaël Monat; Yannick Zakowski (Dagstuhl Artifacts Ser., 2025)