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 | 173 | 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 | 42 | 2021 |

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 | 24 | 2020 |

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 | 20 | 2023 |

Formal reasoning about layered monadic interpreters I Yoon, Y Zakowski, S Zdancewic Proceedings of the ACM on Programming Languages 6 (ICFP), 254-282, 2022 | 16 | 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 | 11 | 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 C Beck, I Yoon, H Chen, Y Zakowski, S Zdancewic arXiv preprint arXiv:2404.16143, 2024 | 3 | 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 | 3 | 2019 |

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 |

A concurrency model based on monadic interpreters: executable semantics for a concurrent subset of LLVM IR N Chappe, L Henrio, 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 |

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 | | 2024 |

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 | | 2024 |

An abstract, certified account of operational game semantics P Borthelle, T Hirschowitz, G Jaber, Y Zakowski | | 2024 |

Effectful Programming across Heterogeneous Computations-Work in Progress J Abou-Samra, Y Zakowski, M Bodin JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, 7-23, 2023 | | 2023 |

33èmes journées francophones des langages applicatifs C Keller, T Bourke, S Blazy, F Bour, G Bury, S Dumbrava, D Gallois-Wong, ... | | 2022 |