Yannick Zakowski

24 papers B 5Misc 1Journal 15Unranked 2
YearRankTypeTitle / Venue / Authors
2026 B conf
Layers of Confluence for Actors.
CPP
Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski
2026 B ed.
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026
CPP
Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau
2025 — conf
An abstract, certified account of operational game semantics.
ESOP (1)
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
2025 — conf
Artifact Report: an Abstract, Certified Account of Operational Game Semantics.
ESOP (1)
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
2025 J jnl
Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq.
J. Funct. Program.
Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic
2025 J jnl
Front Matter, Table of Contents, Preface, Conference Organization.
Dagstuhl Artifacts Ser.
Karine Even-Mendoza, Raphaël Monat, Yannick Zakowski
2025 B conf
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR.
CPP
Nicolas Chappe, Ludovic Henrio, Yannick Zakowski
2025 J jnl
Structural Temporal Logic for Mechanized Program Verification.
Proc. ACM Program. Lang.
Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel
2024 J jnl
A Two-Phase Infinite/Finite Low-Level Memory Model.
CoRR
Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
2024 J jnl
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction.
Proc. ACM Program. Lang.
Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
2024 J jnl
Abstract Interpreters: A Monadic Approach to Modular Verification.
Proc. ACM Program. Lang.
Sébastien Michelland, Yannick Zakowski, Laure Gonnord
2024 J jnl
Structural temporal logic for mechanized program verification.
CoRR
Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel
2023 J jnl
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.
Proc. ACM Program. Lang.
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
2022 J jnl
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.
CoRR
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
2022 J jnl
Formal reasoning about layered monadic interpreters.
Proc. ACM Program. Lang.
Irene Yoon, Yannick Zakowski, Steve Zdancewic
2021 J jnl
Modular, compositional, and executable formal semantics for LLVM IR.
Proc. ACM Program. Lang.
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
2020 J jnl
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction.
CoRR
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020 B conf
An equational theory for weak bisimulation via generalized parameterized coinduction.
CPP
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020 J jnl
Interaction trees: representing recursive and impure programs in Coq.
Proc. ACM Program. Lang.
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2019 J jnl
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).
CoRR
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2019 J jnl
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology.
J. Autom. Reason.
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
2018 Misc conf
Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.
SAC
Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie
2017 — —
Verification of a Concurrent Garbage Collector. (Vérification d'un glaneur de cellules concurrent).
Yannick Zakowski
2017 B conf
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.
ITP
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek