2024
1.
Dan Frumin, Amin Timany, and Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees.
In
POPL 2024,
January 2024.
https://doi.org/10.1145/3632854
[.pdf]- Distinguished paper award
2.
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.
https://doi.org/10.1145/3632851
[.pdf]3.
Amin Timany, Armaël Guéneau, and Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow.
In
POPL 2024,
January 2024.
https://doi.org/10.1145/3632862
[.pdf]2023
4.
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.
https://doi.org/10.1145/3623510
[.pdf]5.
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.
https://doi.org/10.1145/3607859
[.pdf]6.
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.
https://doi.org/10.4230/LIPICS.ECOOP.2023.22
[.pdf]7.
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.
https://doi.org/10.1145/3591279
[.pdf]2022
8.
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.
https://doi.org/10.1145/3563351
[.pdf]9.
Koen Jacobs, Dominique Devriese, and Amin Timany:
Purity of an ST monad: full abstraction by semantically typed back-translation.
In
OOPSLA 2022,
December 2022.
https://doi.org/10.1145/3527326
[.pdf]10.
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 2021,
August 2022.
https://doi.org/10.1109/CSF54842.2022.9919645
[.pdf]11.
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal:
A Logical Approach to Type Soundness.
Submitted for publication,
January 2022.
[.pdf]2021
12.
Amin Timany and Lars Birkedal:
Reasoning About Monotonicity in Separation Logic.
In
CPP 2021,
January 2021.
https://doi.org/10.1145/3437992.3439931
[.pdf (amended after publication)|Coq Development]13.
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.
https://doi.org/10.1145/3434323
[.pdf|Coq Development]14.
Koen Jacobs, Amin Timany, and Dominique Devriese:
Fully Abstract from Static to Gradual.
In
POPL 2021,
January 2021.
https://doi.org/10.1145/3434288
[.pdf|Coq Development]15.
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.
https://doi.org/10.1145/3434287
[.pdf|Coq Development]16.
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal:
Mechanized Logical Relations for Termination-Insensitive Noninterference.
In
POPL 2021,
January 2021.
https://doi.org/10.1145/3434291
[.pdf|Coq Development]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.
https://doi.org/10.1145/3408996
[.pdf|Coq Development]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.
https://doi.org/10.1017/S095679682000015519.
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.
[.pdf|Technical Appendix|Coq Development]20.
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.
https://doi.org/10.1145/3371113
[.pdf|website|talk on youtube]21.
Koen Jacobs, Amin Timany, and Dominique Devriese:
Fully Abstract from Static to Gradual.
In
WGT'20,
January 2020.
[.pdf]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.
https://doi.org/10.1145/3341709
[.pdf|Coq Development|talk on youtube]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.
https://doi.org/10.1145/3340672.3341118
[.pdf]24.
Willem Penninckx, Amin Timany, and Bart Jacobs:
Abstract I/O Specification.
In
CoRR abs/1901.10541 (2019),
January 2019.
[arXiv]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.
https://doi.org/10.1145/3236772
[.pdf|website|talk on youtube]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.
https://doi.org/10.4230/LIPIcs.FSCD.2018.29
[.pdf]27.
Amin Timany:
Contributions in Programming Languages Theory: Logical Relations and Type Theory.
PhD dissertation at KU Leuven,
May 2018.
[.pdf|Lirias|[slides] .pdf]28.
Amin Timany, Léo Stefanesco, Morten Krogh-Jeslpersen, 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.
https://doi.org/10.1145/3158152
[.pdf|Coq Development|talk on youtube]2017
29.
Amin Timany and Matthieu Sozeau:
Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC).
Hosted on
arXiv and HAL,
October 2017.
[arXiv|HAL]30.
Amin Timany, Matthieu Sozeau, and Bart Jacobs:
Cumulative inductive types in Coq.
In
TYPES'17,
May 2017.
[.pdf|[slides] .pdf]31.
Amin Timany, Robbert Krebbers, and Lars Birkedal:
Logical Relations in Iris.
In
CoqPL'17,
January 2017.
[.pdf|[slides] .pdf]32.
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.
https://doi.org/10.1145/3009837.3009855
[.pdf|[slides] .pdf|talk on youtube]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.
https://doi.org/10.4230/LIPIcs.FSCD.2016.30
[.pdf|GitHub|[slides] .pdf]34.
Amin Timany and Bart Jacobs:
Category Theory in Coq 8.5: Extended Version.
Hosted on
KU Leuven Library (lirias),
April 2016.
[Lirias]35.
Amin Timany and Bart Jacobs:
The Category-theoretic Solution of Recursive Ultra-metric Space Equations.
In
CoqPL'17,
January 2016.
[.pdf|Coq Development|[slides] .pdf]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.
https://doi.org/10.1007/978-3-319-25150-9_36
[.pdf|[slides] .pdf]37.
Amin Timany and Bart Jacobs:
Category Theory in Coq 8.5.
In
Coq Workshop 2015,
June 2015.
[arXiv|[slides] .pdf]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.
[Lirias]2013
39.
Amin Timany:
Symmetry Reduction for Reo and Constraint Automata.
MSc thesis at TU Dresden,
May 2013.
[.pdf|[slides] .pdf]