Amin Timany

According to our database, Amin Timany authored at least 40 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.

Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

The Logical Essence of Well-Bracketed Control Flow.

Amin Timany, Armaël Guéneau, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

Modular Denotational Semantics for Effects with Guarded Interaction Trees.

Dan Frumin, Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

J. ACM, 2024

2023

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact.

Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal

Dataset, November, 2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols.

Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., August, 2023

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.

Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal

Proc. ACM Program. Lang., 2023

Modular Verification of State-Based CRDTs in Separation Logic (Artifact).

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal

Dagstuhl Artifacts Ser., 2023

Modular Verification of State-Based CRDTs in Separation Logic.

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal

Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

2022

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact).

Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

Dataset, July, 2022

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact).

Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

Dataset, July, 2022

Modular verification of op-based CRDTs in separation logic.

Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., 2022

Purity of an ST monad: full abstraction by semantically typed back-translation.

Koen Jacobs, Dominique Devriese, Amin Timany

Proc. ACM Program. Lang., 2022

Proving full-system security properties under multiple attacker models on capability machines.

Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization.

Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese

Dataset, September, 2021

Fully abstract from static to gradual.

Koen Jacobs, Amin Timany, Dominique Devriese

Proc. ACM Program. Lang., 2021

Mechanized logical relations for termination-insensitive noninterference.

Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., 2021

Distributed causal memory: modular specification and verification in higher-order distributed separation logic.

Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., 2021

Efficient and provable local capability revocation using uninitialized capabilities.

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal

Proc. ACM Program. Lang., 2021

Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic.

Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal

CoRR, 2021

Reasoning about monotonicity in separation logic.

Amin Timany, Lars Birkedal

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

The future is ours: prophecy variables in separation logic.

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs

Proc. ACM Program. Lang., 2020

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.

Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers

Proc. ACM Program. Lang., 2020

Leibniz equality is isomorphic to Martin-Löf identity, parametrically.

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler

J. Funct. Program., 2020

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report.

Tobias Reinhard, Amin Timany, Bart Jacobs

CoRR, 2020

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems.

Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2020

A separation logic to verify termination of busy-waiting for abrupt program exit.

Tobias Reinhard, Amin Timany, Bart Jacobs

Proceedings of the FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, 2020

2019

Mechanized relational verification of concurrent programs with continuations.

Amin Timany, Lars Birkedal

Proc. ACM Program. Lang., 2019

Abstract I/O Specification.

Willem Penninckx, Amin Timany, Bart Jacobs

CoRR, 2019

Specifying I/O using abstract nested hoare triples in separation logic.

Willem Penninckx, Amin Timany, Bart Jacobs

Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 2019

2018

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST.

Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal

Proc. ACM Program. Lang., 2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer

Proc. ACM Program. Lang., 2018

Cumulative Inductive Types In Coq.

Amin Timany, Matthieu Sozeau

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC).

Amin Timany, Matthieu Sozeau

CoRR, 2017

Interactive proofs in higher-order concurrent separation logic.

Robbert Krebbers, Amin Timany, Lars Birkedal

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Category Theory in Coq 8.5.

Amin Timany, Bart Jacobs

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

2015

First Steps Towards Cumulative Inductive Types in CIC.

Amin Timany, Bart Jacobs

Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015