Amin Timany

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 34

Top Topics

Technical Report

Denotational Semantics

Logical Theories

Top Venues

Proc. ACM Program. Lang.

Publications

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. J. ACM 71 (1) (2024)
Amin Timany, Armaël Guéneau, Lars Birkedal
The Logical Essence of Well-Bracketed Control Flow. Proc. ACM Program. Lang. 8 (POPL) (2024)
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. Proc. ACM Program. Lang. 8 (POPL) (2024)
Dan Frumin, Amin Timany, Lars Birkedal
Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proc. ACM Program. Lang. 8 (POPL) (2024)
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
Modular Verification of State-Based CRDTs in Separation Logic (Artifact). Dagstuhl Artifacts Ser. 9 (2) (2023)
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
Modular Verification of State-Based CRDTs in Separation Logic. ECOOP (2023)
Dan Frumin, Amin Timany, Lars Birkedal
Modular Denotational Semantics for Effects with Guarded Interaction Trees. CoRR (2023)
Koen Jacobs, Dominique Devriese, Amin Timany
Purity of an ST monad: full abstraction by semantically typed back-translation. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal
Modular verification of op-based CRDTs in separation logic. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
Proving full-system security properties under multiple attacker models on capability machines. CSF (2022)
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal
Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. CoRR (2021)
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
Distributed causal memory: modular specification and verification in higher-order distributed separation logic. Proc. ACM Program. Lang. 5 (POPL) (2021)
Koen Jacobs, Amin Timany, Dominique Devriese
Fully abstract from static to gradual. Proc. ACM Program. Lang. 5 (POPL) (2021)
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang. 5 (POPL) (2021)
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5 (POPL) (2021)
Amin Timany, Lars Birkedal
Reasoning about monotonicity in separation logic. CPP (2021)
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. ESOP (2020)
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. CoRR (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. CoRR (2020)
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler
Leibniz equality is isomorphic to Martin-Löf identity, parametrically. J. Funct. Program. 30 (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A separation logic to verify termination of busy-waiting for abrupt program exit. FTfJP@ECOOP (2020)
Amin Timany, Lars Birkedal
Mechanized relational verification of concurrent programs with continuations. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Willem Penninckx, Amin Timany, Bart Jacobs
Specifying I/O using abstract nested hoare triples in separation logic. FTfJP@ECOOP (2019)
Willem Penninckx, Amin Timany, Bart Jacobs
Abstract I/O Specification. CoRR (2019)
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. Proc. ACM Program. Lang. 2 (POPL) (2018)
Amin Timany, Matthieu Sozeau
Cumulative Inductive Types In Coq. FSCD (2018)
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Robbert Krebbers, Amin Timany, Lars Birkedal
Interactive proofs in higher-order concurrent separation logic. POPL (2017)
Amin Timany, Matthieu Sozeau
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). CoRR (2017)
Amin Timany, Bart Jacobs
Category Theory in Coq 8.5. FSCD (2016)
Amin Timany, Bart Jacobs
First Steps Towards Cumulative Inductive Types in CIC. ICTAC (2015)
Amin Timany, Bart Jacobs
Category Theory in Coq 8.5. CoRR (2015)