Publications

Scholar Profile DBLP entry
2025
1.
Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It. In FSCD 2025, June 2025, doi: 10.4230/LIPIcs.FSCD.2025.30.
2.
Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, and Lars Birkedal. Context-Dependent Effects in Guarded Interaction Trees. In ESOP 2025: European Symposium on Programming, May 2025, doi: 10.1007/978-3-031-91121-7_12.
3.
Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It. In TYPES'25, May 2025.
2024
4.
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A Logical Approach to Type Soundness. In JACM, June 2024, doi: 10.1145/3676954.
5.
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.
6.
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.
7.
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
8.
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.
9.
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.
10.
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In ECOOP 2023, July 2023, doi: 10.4230/LIPICS.ECOOP.2023.22.
11.
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.
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.
13.
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.
14.
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. Proving full-system security properties under multiple attacker models on capability machines. In CSF 2022, August 2022, doi: 10.1109/CSF54842.2022.9919645.
2021
15.
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.
16.
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.
17.
Koen Jacobs, Amin Timany, and Dominique Devriese. Fully Abstract from Static to Gradual. In POPL 2021, January 2021, doi: 10.1145/3434288.
18.
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.
19.
Amin Timany and Lars Birkedal. Reasoning About Monotonicity in Separation Logic. In CPP 2021, January 2021, doi: 10.1145/3437992.3439931.
2020
20.
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.
21.
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.
22.
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In ESOP 2020: European Symposium on Programming, April 2020, doi: 10.1007/978-3-030-44914-8_13.
23.
Koen Jacobs, Amin Timany, and Dominique Devriese. Fully Abstract from Static to Gradual. In WGT'20, January 2020.
24.
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
25.
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.
26.
Willem Penninckx, Amin Timany, and Bart Jacobs. Specifying I/O Using Abstract Nested Hoare Triples in Separation Logic. In Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, July 2019, doi: 10.1145/3340672.3341118.
27.
Willem Penninckx, Amin Timany, and Bart Jacobs. Abstract I/O Specification. In CoRR abs/1901.10541 (2019), January 2019.
2018
28.
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.
29.
Amin Timany and Matthieu Sozeau. Cumulative Inductive Types In Coq. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 2018, doi: 10.4230/LIPIcs.FSCD.2018.29.
30.
Amin Timany. Contributions in Programming Languages Theory: Logical Relations and Type Theory. PhD dissertation at KU Leuven, May 2018.
31.
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.
2017
32.
Amin Timany and Matthieu Sozeau. Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC). Hosted on arXiv and HAL, October 2017.
33.
Amin Timany, Matthieu Sozeau, and Bart Jacobs. Cumulative inductive types in Coq. In TYPES'17, May 2017.
34.
Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, January 2017, doi: 10.1145/3009837.3009855.
35.
Amin Timany, Robbert Krebbers, and Lars Birkedal. Logical Relations in Iris. In CoqPL'17, January 2017.
2016
36.
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 2016, doi: 10.4230/LIPIcs.FSCD.2016.30.
37.
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5: Extended Version. Hosted on KU Leuven Library (lirias), April 2016.
38.
Amin Timany and Bart Jacobs. The Category-theoretic Solution of Recursive Ultra-metric Space Equations. In CoqPL'16, January 2016.
2015
39.
Amin Timany and Bart Jacobs. First Steps Towards Cumulative Inductive Types in CIC. In Proceedings of Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium, October 2015, doi: 10.1007/978-3-319-25150-9_36.
40.
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In Coq Workshop 2015, June 2015.
2014
41.
Amin Timany and Bart Jacobs. A Local Shape Analysis Based on Separation Logic: Detailed Presentation and Soundness Proof. Hosted on KU Leuven Library (lirias), May 2014.
2013
42.
Amin Timany. Symmetry Reduction for Reo and Constraint Automata. MSc thesis at TU Dresden, May 2013.