| Interaction trees: representing recursive and impure programs in Coq L Xia, Y Zakowski, P He, CK Hur, G Malecha, BC Pierce, S Zdancewic Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019 | 196 | 2019 |
| Modular, compositional, and executable formal semantics for LLVM IR Y Zakowski, C Beck, I Yoon, I Zaichuk, V Zaliva, S Zdancewic Proceedings of the ACM on Programming Languages 5 (ICFP), 1-30, 2021 | 50 | 2021 |
| Choice trees: Representing nondeterministic, recursive, and impure programs in coq N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic Proceedings of the ACM on Programming Languages 7 (POPL), 1770-1800, 2023 | 26 | 2023 |
| An equational theory for weak bisimulation via generalized parameterized coinduction Y Zakowski, P He, CK Hur, S Zdancewic Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 26 | 2020 |
| Formal reasoning about layered monadic interpreters I Yoon, Y Zakowski, S Zdancewic Proceedings of the ACM on Programming Languages 6 (ICFP), 254-282, 2022 | 20 | 2022 |
| Verifying a concurrent garbage collector using a rely-guarantee methodology Y Zakowski, D Cachera, D Demange, G Petri, D Pichardie, ... Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 12 | 2017 |
| Compilation of linearizable data structures-a mechanised RG logic for semantic refinement Y Zakowski, D Cachera, D Demange, D Pichardie Symposium on Applied Computing, 2017 | 5 | 2017 |
| A two-phase infinite/finite low-level memory model: Reconciling integer–pointer casts, finite space, and undef at the llvm ir level of abstraction C Beck, I Yoon, H Chen, Y Zakowski, S Zdancewic Proceedings of the ACM on Programming Languages 8 (ICFP), 789-817, 2024 | 4 | 2024 |
| Verifying a concurrent garbage collector with a rely-guarantee methodology Y Zakowski, D Cachera, D Demange, G Petri, D Pichardie, ... Journal of Automated Reasoning 63, 489-515, 2019 | 4 | 2019 |
| A Two-Phase Infinite/Finite Low-Level Memory Model C Beck, I Yoon, H Chen, Y Zakowski, S Zdancewic arXiv preprint arXiv:2404.16143, 2024 | 3 | 2024 |
| Verification of a Concurrent Garbage Collector Y Zakowski École normale supérieure de Rennes, 2017 | 3 | 2017 |
| Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement Y Zakowski, D Cachera, D Demange, D Pichardie Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 1881-1890, 2018 | 2 | 2018 |
| Abstract Interpreters: A Monadic Approach to Modular Verification S Michelland, Y Zakowski, L Gonnord Proceedings of the ACM on Programming Languages 8 (ICFP), 602-629, 2024 | 1 | 2024 |
| A concurrency model based on monadic interpreters: executable semantics for a concurrent subset of LLVM IR N Chappe, L Henrio, Y Zakowski | 1 | 2024 |
| An abstract, certified account of operational game semantics P Borthelle, T Hirschowitz, G Jaber, Y Zakowski | 1 | 2024 |
| Abstract Interpreters: a Monadic Approach to Modular Verification (DRAFT) S Michelland, Y Zakowski, L Gonnord | 1 | 2024 |
| Choice trees N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic POPL, 2023 | 1 | 2023 |
| Programming with information flow-control Y Zakowski Internship report, Magistère Informatique et Télécommunication, ENS Cachan …, 2012 | 1 | 2012 |
| Monadic Interpreters for Concurrent Memory Models N Chappe, L Henrio, Y Zakowski CPP’25, 283, 2025 | | 2025 |
| Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR N Chappe, L Henrio, Y Zakowski Proceedings of the 14th ACM SIGPLAN International Conference on Certified …, 2025 | | 2025 |