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 | 144 | 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 | 31 | 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 | 20* | 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 | 12 | 2022 |

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

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

Verification of a Concurrent Garbage Collector Y Zakowski École normale supérieure de Rennes, 2017 | 3 | 2017 |

Choice trees N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic POPL, 2023 | 2 | 2023 |

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 | 2 | 2019 |

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 |

Programming with information flow-control Y Zakowski Internship report, Magistère Informatique et Télécommunication, ENS Cachan …, 2012 | 1 | 2012 |

Abstract Interpreters: a Monadic Approach to Modular Verification (DRAFT) S Michelland, Y Zakowski, L Gonnord | | 2024 |

Effectful Programming across Heterogeneous Computations—Work in Progress J Abou Samra, M Bodin, Y Zakowski 34 èmes Journées Francophones des Langages Applicatifs, 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 |

Compilation of Linearizable Data Structures Y Zakowski, D Cachera, D Demange, D Pichardie ENS Rennes; IRISA, Inria Rennes; Université Rennes 1, 2017 | | 2017 |

Generation of polynomial inequalities as invariants Y Zakowski | | 2013 |

THE LOGIC AND SEMANTICS GROUP L Birkedal, R Clouston, T Dinsdale-Young, F Sieczkowski, K Svendsen, ... | | 2011 |

Nondeterministic, Recursive, and Impure Programs in Coq N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic AFADL 2023, 37, 0 | | |

Games and Strategies using Coinductive Types P Borthelle, T Hirschowitz, G Jaber, Y Zakowski 29th International Conference on Types for Proofs and Programs TYPES 2023 …, 0 | | |