In 2020, Amin Timany joined the Logic and Semantics research group at the Department of Computer Science as a Tenure Track Assistant Professor. Amin's research is mainly concerned with program verification. 

Program verification is a very important field of research as our lives are more and more entangled with computer systems. Amin's approach to program verification is a formal and foundational approach where he uses formal and mathematical tools for reasoning about programs. In particular, his research is focused on development and application of program logics to program verification. A program logic is a mathematical theory (based on mathematical logic) which is designed specifically for reasoning about programs at a high level of abstraction. This enables reasoning about programs based on their semantics (their precise behavior) which is often too complex to directly reason about for advanced, state-of-the-art programs and programming languages.

Amin uses proof assistants (software that checks correctness of mathematical proofs) in his work both to establish the soundness of the program logics that he studies, and for verification of programs based on these program logics. Establishing correctness of a mathematical theory in a proof assistant is arguably the highest level of mathematical rigor attainable. In the past several years of his research in this field, Amin has extensively used and contributed to the Iris program logic framework (https://iris-project.org) and the Coq proof assistant (https://coq.inria.fr). In addition to program verification, Amin is also more broadly interested in theory of programming languages, compilers, type theory, mathematical logic, and foundations of mathematics.  

Academic background

Before joining the Department of Computer Science at Aarhus University, Amin held a prestigious postdoctoral fellowship from the Flemish research fund (FWO) in Flanders, Belgium. During this fellowship he was working as a member of the DistriNet research group at the computer science department of KU Leuven, Leuven, Belgium. Amin also obtained his PhD from KU Leuven in May 2018 under the aegis of Prof. Bart Jacobs. During his PhD, Amin made several research visits to, and collaborated with, leading international researchers including Prof. Derek Dreyer (MPI-SWS, Saarbrücken, Germany), Prof. Lars Birkedal (Aarhus University), Dr. Matthieu Sozeau (Inria, Nantes, France).

Top 3 papers

• Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal: "Mechanized Logical Relations for Termination-Insensitive Noninterference". In POPL 2021, January 2021. In this paper, Amin and his collaborators established correctness of an information-flow type system. That is, they showed that a type system designed to guarantee noninterference (a security property) is correct, i.e., well-typed programs do indeed have the noninterference property. This is the most expressive type system for noninterference proven correct to date.
• 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. This work presents Aneris, a program logic build on top of the Iris program logic framework for reasoning about distributed systems. In enables both reasoning about distributed systems and their clients in a modular fashion, e.g., the server and the client are proven correct independently but are guaranteed their communication is always correct. This work is also the foundation for other recent work (published at POPL'21) by Amin and his collaborators which establishes correctness of a distributed database system and its clients.
• 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. This work proves the correctness a Haskell-style ST monad which safely encapsulates state in an otherwise pure programming language. This work establishes that the expected program equivalences and program refinements for a pure programming language also hold in the presence of the ST monad. This was an open problem for about two decades prior to this paper.