Scholar Profile
ORCiD
DBLP entry2024
1.
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal.
A Logical Approach to Type Soundness.
Accepted for publication in
JACM,
June 2024.
- Links:
.pdf
Journal Paper
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.
Journal Paper
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.
Journal Paper
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.
Journal Paper
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.
Journal Paper
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.
Journal Paper
7.
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.
Conference Paper
8.
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.
Journal Paper
2022
9.
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.
Journal Paper
10.
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.
Journal Paper
11.
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.
Conference Paper
2021
12.
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.
- Links:
DOI
.pdf
Coq Development
Journal Paper
13.
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.
- Links:
DOI
.pdf
Coq Development
Journal Paper
14.
Koen Jacobs, Amin Timany, and Dominique Devriese.
Fully Abstract from Static to Gradual.
In
POPL 2021,
January 2021, doi: 10.1145/3434288.
- Links:
DOI
.pdf
Coq Development
Journal Paper
15.
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.
- Links:
DOI
.pdf
Coq Development
Journal Paper
16.
Amin Timany and Lars Birkedal.
Reasoning About Monotonicity in Separation Logic.
In
CPP 2021,
January 2021, doi: 10.1145/3437992.3439931.
Conference Paper
2020
17.
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.
- Links:
DOI
.pdf
Coq Development
Journal Paper
18.
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.
- Links:
DOI
Journal Paper
19.
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.
- Links:
DOI
.pdf
Technical Appendix
Coq Development
Conference Paper
20.
Koen Jacobs, Amin Timany, and Dominique Devriese.
Fully Abstract from Static to Gradual.
In
WGT'20,
January 2020.
- Links:
.pdf
Unpublished Workshop Paper
21.
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.
- Links:
DOI
.pdf
website
talk on youtube
Journal Paper
2019
22.
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.
- Links:
DOI
.pdf
Coq Development
talk on youtube
Journal Paper
23.
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.
Conference Paper
24.
Willem Penninckx, Amin Timany, and Bart Jacobs.
Abstract I/O Specification.
In
CoRR abs/1901.10541 (2019),
January 2019.
- Links:
arXiv
Technical Report
2018
25.
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.
- Links:
DOI
.pdf
website
talk on youtube
Journal Paper
26.
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.
Conference Paper
27.
Amin Timany.
Contributions in Programming Languages Theory: Logical Relations and Type Theory.
PhD dissertation at KU Leuven,
May 2018.
- Links:
.pdf
Lirias
[slides] .pdf
PhD dissertation
28.
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.
- Links:
DOI
.pdf
Coq Development
talk on youtube
Journal Paper
2017
29.
Amin Timany and Matthieu Sozeau.
Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC).
Hosted on
arXiv and HAL,
October 2017.
Technical Report
30.
Amin Timany, Matthieu Sozeau, and Bart Jacobs.
Cumulative inductive types in Coq.
In
TYPES'17,
May 2017.
- Links:
.pdf
[slides] .pdf
Unpublished Workshop Paper
31.
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.
- Links:
DOI
.pdf
[slides] .pdf
talk on youtube
Conference Paper
32.
Amin Timany, Robbert Krebbers, and Lars Birkedal.
Logical Relations in Iris.
In
CoqPL'17,
January 2017.
- Links:
.pdf
[slides] .pdf
Unpublished Workshop Paper
2016
33.
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.
- Links:
DOI
.pdf
GitHub
[slides] .pdf
Conference Paper
34.
Amin Timany and Bart Jacobs.
Category Theory in Coq 8.5: Extended Version.
Hosted on
KU Leuven Library (lirias),
April 2016.
- Links:
Lirias
Technical Report
35.
Amin Timany and Bart Jacobs.
The Category-theoretic Solution of Recursive Ultra-metric Space Equations.
In
CoqPL'17,
January 2016.
- Links:
.pdf
Coq Development
[slides] .pdf
Unpublished Workshop Paper
2015
36.
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.
- Links:
DOI
.pdf
[slides] .pdf
Conference Paper
37.
Amin Timany and Bart Jacobs.
Category Theory in Coq 8.5.
In
Coq Workshop 2015,
June 2015.
- Links:
arXiv
[slides] .pdf
Unpublished Workshop Paper
2014
38.
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.
- Links:
Lirias
Technical Report
2013
39.
Amin Timany.
Symmetry Reduction for Reo and Constraint Automata.
MSc thesis at TU Dresden,
May 2013.
- Links:
.pdf
[slides] .pdf
MSc thesis