Journal Publications

These works are published in scientific journals.

2025

20. In ICFP 2025 Journal Paper
Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, and Lars Birkedal. Reasoning about Weak Isolation Levels in Separation Logic. In ICFP 2025, August 2025, doi: 10.1145/3747515.

2024

19. In JACM Journal Paper
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A Logical Approach to Type Soundness. In JACM, June 2024, doi: 10.1145/3676954.
18. In POPL 2024 Journal Paper
Dan Frumin, Amin Timany, and Lars Birkedal. Modular Denotational Semantics for Effects with Guarded Interaction Trees. In POPL 2024, January 2024, doi: 10.1145/3632854.
17. In POPL 2024 Journal Paper
Amin Timany, Armaël Guéneau, and Lars Birkedal. The Logical Essence of Well-Bracketed Control Flow. In POPL 2024, January 2024, doi: 10.1145/3632862.
16. In POPL 2024 Journal Paper
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. In POPL 2024, January 2024, doi: 10.1145/3632851.

2023

15. In JACM Journal Paper
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. In JACM, December 2023, doi: 10.1145/3623510.
14. In ICFP 2023 Journal Paper
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. In ICFP 2023, August 2023, doi: 10.1145/3607859.
13. In PLDI 2023 Journal Paper
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal. VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. In PLDI 2023, June 2023, doi: 10.1145/3591279.

2022

12. In OOPSLA 2022 Journal Paper
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular verification of op-based CRDTs in separation logic. In OOPSLA 2022, December 2022, doi: 10.1145/3563351.
11. In OOPSLA 2022 Journal Paper
Koen Jacobs, Dominique Devriese, and Amin Timany. Purity of an ST monad: full abstraction by semantically typed back-translation. In OOPSLA 2022, December 2022, doi: 10.1145/3527326.

2021

10. In POPL 2021 Journal Paper
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic. In POPL 2021, January 2021, doi: 10.1145/3434323.
9. In POPL 2021 Journal Paper
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal. Efficient and Provable Local Capability Revocation using Uninitialized Capabilities. In POPL 2021, January 2021, doi: 10.1145/3434287.
8. In POPL 2021 Journal Paper
Koen Jacobs, Amin Timany, and Dominique Devriese. Fully Abstract from Static to Gradual. In POPL 2021, January 2021, doi: 10.1145/3434288.
7. In POPL 2021 Journal Paper
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. Mechanized Logical Relations for Termination-Insensitive Noninterference. In POPL 2021, January 2021, doi: 10.1145/3434291.

2020

6. In PACMPL 4(ICFP): 114:1-114:29 (2020) Journal Paper
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris. In PACMPL 4(ICFP): 114:1-114:29 (2020), June 2020, doi: 10.1145/3408996.
5. In Journal of Functional Programming (JFP) Journal Paper
Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler. Leibniz equality is isomorphic to Martin-Löf identity, parametrically. In Journal of Functional Programming (JFP), May 2020, doi: 10.1017/S0956796820000155.
4. In PACMPL 4(POPL): 45:1-45:32 (2020) Journal Paper
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. In PACMPL 4(POPL): 45:1-45:32 (2020), January 2020, doi: 10.1145/3371113.

2019

3. In PACMPL 3(ICFP): 105:1-105:28 (2019) Journal Paper
Amin Timany and Lars Birkedal. Mechanized Relational Verification of Concurrent Programs with Continuations. In PACMPL 3(ICFP): 105:1-105:28 (2019), August 2019, doi: 10.1145/3341709.

2018

2. In PACMPL 2(ICFP): 77:1--77:30 (2018) Journal Paper
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. In PACMPL 2(ICFP): 77:1--77:30 (2018), August 2018, doi: 10.1145/3236772.
1. In PACMPL 2(POPL): 64:1-64:28 (2018) Journal Paper
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. In PACMPL 2(POPL): 64:1-64:28 (2018), January 2018, doi: 10.1145/3158152.