First Steps Towards Cumulative Inductive Types in CIC. - Amin Timany; Bart Jacobs 002 (ICTAC, 2015)

Category Theory in Coq 8.5. - Amin Timany; Bart Jacobs 002 (FSCD, 2016)

Interactive proofs in higher-order concurrent separation logic. - Robbert Krebbers; Amin Timany; Lars Birkedal (POPL, 2017)

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). - Amin Timany; Matthieu Sozeau (CoRR, 2017)

Cumulative Inductive Types In Coq. - Amin Timany; Matthieu Sozeau (FSCD, 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 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)

Specifying I/O using abstract nested hoare triples in separation logic. - Willem Penninckx; Amin Timany; Bart Jacobs 002 (FTfJP@ECOOP, 2019)

Abstract I/O Specification. - Willem Penninckx; Amin Timany; Bart Jacobs 002 (CoRR, 2019)

Mechanized relational verification of concurrent programs with continuations. - Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2019)

A separation logic to verify termination of busy-waiting for abrupt program exit. - Tobias Reinhard; Amin Timany; Bart Jacobs 002 (FTfJP@ECOOP, 2020)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. - Morten Krogh-Jespersen; Amin Timany; Marit Edna Ohlenbusch; Simon Oddershede Gregersen; Lars Birkedal (ESOP, 2020)

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. - Tobias Reinhard; Amin Timany; Bart Jacobs 002 (CoRR, 2020)

Leibniz equality is isomorphic to Martin-Löf identity, parametrically. - Andreas Abel 001; Jesper Cockx; Dominique Devriese; Amin Timany; Philip Wadler (J. Funct. Program., 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)

The future is ours: prophecy variables in separation logic. - Ralf Jung 002; Rodolphe Lepigre; Gaurav Parthasarathy; Marianna Rapoport; Amin Timany; Derek Dreyer; Bart Jacobs 002 (Proc. ACM Program. Lang., 2020)

Reasoning about monotonicity in separation logic. - Amin Timany; Lars Birkedal (CPP, 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)

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)

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)

Mechanized logical relations for termination-insensitive noninterference. - Simon Oddershede Gregersen; Johan Bay; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Fully abstract from static to gradual. - Koen Jacobs; Amin Timany; Dominique Devriese (Proc. ACM Program. Lang., 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 (Zenodo, 2021)

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 (CSF, 2022)

Purity of an ST monad: full abstraction by semantically typed back-translation. - Koen Jacobs; Dominique Devriese; Amin Timany (Proc. ACM Program. Lang., 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)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)

Modular Verification of State-Based CRDTs in Separation Logic. - Abel Nieto; Arnaud Daby-Seesaram; Léon Gondelman; Amin Timany; Lars Birkedal (ECOOP, 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)

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. - Zongyuan Liu 001; Sergei Stepanenko; Jean Pichon-Pharabod; Amin Timany; Aslan Askarov; Lars Birkedal (Proc. ACM Program. Lang., 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., 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 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 (Zenodo, 2023)

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)

Modular Denotational Semantics for Effects with Guarded Interaction Trees. - Dan Frumin; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2024)

The Logical Essence of Well-Bracketed Control Flow. - Amin Timany; Armaël Guéneau; Lars Birkedal (Proc. ACM Program. Lang., 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., 2024)

A Logical Approach to Type Soundness. - Amin Timany; Robbert Krebbers; Derek Dreyer; Lars Birkedal (J. ACM, 2024)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (ESOP (2), 2025)

Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It. - Sergei Stepanenko; Amin Timany (FSCD, 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)

Reasoning about Weak Isolation Levels in Separation Logic. - Anders Alnor Mathiasen; Léon Gondelman; Léon Ducruet; Amin Timany; Lars Birkedal (CoRR, 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)