Segui
Yannick Zakowski
Yannick Zakowski
Email verificata su inria.fr
Titolo
Citata da
Citata da
Anno
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
1792019
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
442021
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
252020
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
222023
Formal reasoning about layered monadic interpreters
I Yoon, Y Zakowski, S Zdancewic
Proceedings of the ACM on Programming Languages 6 (ICFP), 254-282, 2022
162022
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
112017
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
52017
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
42019
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
32024
Verification of a Concurrent Garbage Collector
Y Zakowski
École normale supérieure de Rennes, 2017
32017
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
22018
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
12024
A concurrency model based on monadic interpreters: executable semantics for a concurrent subset of LLVM IR
N Chappe, L Henrio, Y Zakowski
12024
Abstract Interpreters: a Monadic Approach to Modular Verification (DRAFT)
S Michelland, Y Zakowski, L Gonnord
12024
Choice trees
N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic
POPL, 2023
12023
Programming with information flow-control
Y Zakowski
Internship report, Magistère Informatique et Télécommunication, ENS Cachan …, 2012
12012
Structural temporal logic for mechanized program verification
E Ioannidis, Y Zakowski, S Zdancewic, S Angel
arXiv preprint arXiv:2410.14906, 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
Il sistema al momento non può eseguire l'operazione. Riprova più tardi.
Articoli 1–20