2024
1.
Dan Frumin, Amin Timany, and Lars Birkedal: Modular Denotational Semantics for Effects with Guarded Interaction Trees. In POPL 2024, January 2024.
    Journal Paper
    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.
      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.
        Journal Paper
        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.
          Journal Paper
          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.
            Journal Paper
            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.
              Conference Paper
              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.
                Journal Paper
                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.
                  Journal Paper
                  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.
                    Journal Paper
                    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.
                      Conference Paper
                      11.
                      Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal: A Logical Approach to Type Soundness. Submitted for publication, January 2022.
                        Journal Paper
                        2021
                        12.
                        Amin Timany and Lars Birkedal: Reasoning About Monotonicity in Separation Logic. In CPP 2021, January 2021.
                          Conference Paper
                          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.
                            Journal Paper
                            14.
                            Koen Jacobs, Amin Timany, and Dominique Devriese: Fully Abstract from Static to Gradual. In POPL 2021, January 2021.
                              Journal Paper
                              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.
                                Journal Paper
                                16.
                                Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal: Mechanized Logical Relations for Termination-Insensitive Noninterference. In POPL 2021, January 2021.
                                  Journal 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.
                                    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.
                                      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.
                                        Conference Paper
                                        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.
                                          Journal Paper
                                          21.
                                          Koen Jacobs, Amin Timany, and Dominique Devriese: Fully Abstract from Static to Gradual. In WGT'20, January 2020.
                                            Unpublished Workshop 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.
                                              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.
                                                Conference Paper
                                                24.
                                                Willem Penninckx, Amin Timany, and Bart Jacobs: Abstract I/O Specification. In CoRR abs/1901.10541 (2019), January 2019.
                                                  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.
                                                    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.
                                                      Conference Paper
                                                      27.
                                                      Amin Timany: Contributions in Programming Languages Theory: Logical Relations and Type Theory. PhD dissertation at KU Leuven, May 2018.
                                                        PhD dissertation
                                                        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.
                                                          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.
                                                              Unpublished Workshop Paper
                                                              31.
                                                              Amin Timany, Robbert Krebbers, and Lars Birkedal: Logical Relations in Iris. In CoqPL'17, January 2017.
                                                                Unpublished Workshop Paper
                                                                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.
                                                                  Conference 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.
                                                                    Conference Paper
                                                                    34.
                                                                    Amin Timany and Bart Jacobs: Category Theory in Coq 8.5: Extended Version. Hosted on KU Leuven Library (lirias), April 2016.
                                                                      Technical Report
                                                                      35.
                                                                      Amin Timany and Bart Jacobs: The Category-theoretic Solution of Recursive Ultra-metric Space Equations. In CoqPL'17, January 2016.
                                                                        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.
                                                                          Conference Paper
                                                                          37.
                                                                          Amin Timany and Bart Jacobs: Category Theory in Coq 8.5. In Coq Workshop 2015, June 2015.
                                                                            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.
                                                                              Technical Report
                                                                              2013
                                                                              39.
                                                                              Amin Timany: Symmetry Reduction for Reo and Constraint Automata. MSc thesis at TU Dresden, May 2013.
                                                                                MSc thesis