2021
[1]
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
    [2]
    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
      [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]
        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
          [5]
          Amin Timany and Lars Birkedal: Reasoning About Monotonicity in Separation Logic. In CPP 2021, January 2021. https://doi.org/10.1145/3437992.3439931 [.pdf|Coq Development]
            Conference 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]
                                        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
                                          [21]
                                          Amin Timany, Robbert Krebbers, and Lars Birkedal: Logical Relations in Iris. In CoqPL'17, January 2017. [.pdf|[slides] .pdf]
                                            Unpublished Workshop 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