Journal Publications

These works are published in scientific journals.
2024
1.
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A Logical Approach to Type Soundness. In JACM, June 2024, doi: 10.1145/3676954.
2.
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.
3.
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.
4.
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
5.
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.
6.
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.
7.
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
8.
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.
9.
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.
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.
11.
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.
12.
Koen Jacobs, Amin Timany, and Dominique Devriese. Fully Abstract from Static to Gradual. In POPL 2021, January 2021, doi: 10.1145/3434288.
13.
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
14.
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.
15.
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.
16.
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
17.
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
18.
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.
19.
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.