2021
[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]
    Journal Paper
    [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]
      Journal Paper
      [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]
        Journal Paper
        [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]
          Journal Paper
          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]
            Journal Paper
            [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
              Journal Paper
              [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]
                Conference Paper
                [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]
                  Journal Paper
                  [10]
                  Koen Jacobs, Amin Timany, and Dominique Devriese: Fully Abstract from Static to Gradual. In WGT'20, January 2020. [.pdf]
                    Unpublished Workshop Paper
                    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]
                      Journal Paper
                      [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]
                        Conference Paper
                        [13]
                        Willem Penninckx, Amin Timany, and Bart Jacobs: Abstract I/O Specification. In CoRR abs/1901.10541 (2019), January 2019. [arXiv]
                          Technical Report
                          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]
                            Journal Paper
                            [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]
                              Conference Paper
                              [16]
                              Amin Timany: Contributions in Programming Languages Theory: Logical Relations and Type Theory. PhD dissertation at KU Leuven, May 2018. [.pdf|Lirias|[slides] .pdf]
                                PhD dissertation
                                [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]
                                  Journal Paper
                                  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]
                                    Technical Report
                                    [19]
                                    Amin Timany, Matthieu Sozeau, and Bart Jacobs: Cumulative inductive types in Coq. In TYPES'17, May 2017. [.pdf|[slides] .pdf]
                                      Unpublished Workshop Paper
                                      [20]
                                      Amin Timany, Robbert Krebbers, and Lars Birkedal: Logical Relations in Iris. In CoqPL'17, January 2017. [.pdf|[slides] .pdf]
                                        Unpublished Workshop Paper
                                        [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]
                                          Conference Paper
                                          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]
                                            Conference Paper
                                            [23]
                                            Amin Timany and Bart Jacobs: Category Theory in Coq 8.5: Extended Version. Hosted on KU Leuven Library (lirias), April 2016. [Lirias]
                                              Technical Report
                                              [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]
                                                Unpublished Workshop Paper
                                                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]
                                                  Conference Paper
                                                  [26]
                                                  Amin Timany, Bart Jacobs: Category Theory in Coq 8.5. In Coq Workshop 2015, June 2015. [arXiv|[slides] .pdf]
                                                    Unpublished Workshop Paper
                                                    [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]
                                                      Technical Report
                                                      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]
                                                        Technical Report
                                                        2013
                                                        [29]
                                                        Amin Timany: Symmetry Reduction for Reo and Constraint Automata. MSc thesis at TU Dresden, May 2013. [.pdf|[slides] .pdf]
                                                          MSc thesis