2021
[1]
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]
[2]
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]
[3]
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]
[4]
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]
[5]
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
[6]
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.
PACMPL 4(ICFP): 114:1-114:29 (2020),
June 2020.
https://doi.org/10.1145/3408996
[.pdf|Coq Development]
[7]
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/S0956796820000155
[8]
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]
[9]
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]
[10]
Koen Jacobs, Amin Timany, and Dominique Devriese:
Fully Abstract from Static to Gradual.
In
WGT'20,
January 2020.
[.pdf]
2019
[11]
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]
[12]
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]
[13]
Willem Penninckx, Amin Timany, and Bart Jacobs:
Abstract I/O Specification.
In
CoRR abs/1901.10541 (2019),
January 2019.
[arXiv]
2018
[14]
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.
In
PACMPL 2(ICFP): 77:1--77:30 (2018),
August 2018.
https://doi.org/10.1145/3236772
[.pdf|website|talk on youtube]
[15]
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]
[16]
Amin Timany:
Contributions in Programming Languages Theory: Logical Relations and Type Theory.
PhD dissertation at KU Leuven,
May 2018.
[.pdf|Lirias|[slides] .pdf]
[17]
Amin Timany, Léo Stefanesco, Morten Krogh-Jeslpersen, 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
[18]
Amin Timany and Matthieu Sozeau:
Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC).
Hosted on
arXiv and HAL,
October 2017.
[arXiv|HAL]
[19]
Amin Timany, Matthieu Sozeau, and Bart Jacobs:
Cumulative inductive types in Coq.
In
TYPES'17,
May 2017.
[.pdf|[slides] .pdf]
[20]
Amin Timany, Robbert Krebbers, and Lars Birkedal:
Logical Relations in Iris.
In
CoqPL'17,
January 2017.
[.pdf|[slides] .pdf]
[21]
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
[22]
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]
[23]
Amin Timany and Bart Jacobs:
Category Theory in Coq 8.5: Extended Version.
Hosted on
KU Leuven Library (lirias),
April 2016.
[Lirias]
[24]
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
[25]
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]
[26]
Amin Timany, Bart Jacobs:
Category Theory in Coq 8.5.
In
Coq Workshop 2015,
June 2015.
[arXiv|[slides] .pdf]
[27]
Amin Timany and Bart Jacobs:
First Steps Towards Cumulative Inductive Types in CIC: Extended Version.
Hosted on
KU Leuven Library (lirias),
March 2015.
[Lirias]
2014
[28]
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
[29]
Amin Timany:
Symmetry Reduction for Reo and Constraint Automata.
MSc thesis at TU Dresden,
May 2013.
[.pdf|[slides] .pdf]