معرفی
Amin Timany is an Associate Professor in the Department of Computer Science at Aarhus University, Denmark, where he conducts research in programming languages, type theory, and formal verification. He is a member of the Logic and Semantics Group and actively contributes to the development of logical relations, separation logic, and proof assistants such as Coq and Iris.
He holds a PhD in Computer Science from KU Leuven (2018) and was previously a postdoctoral fellow with FWO at KU Leuven. His research focuses on mechanized semantics, program equivalence, concurrency, and distributed systems verification. He is particularly known for solving the long-standing problem of proving encapsulation in the ST monad using logical relations.
His recent publications span top-tier venues including POPL, ICFP, PLDI, and CPP, with key contributions in guarded interaction trees, higher-order separation logic (e.g., Trillium), and modular verification of CRDTs and virtual machines. His work emphasizes formalization and mechanization in Coq, often within the Iris framework.
He has served on numerous program committees and has chaired conferences such as CPP and sessions at CoqPL. Notably, his paper 'Modular Denotational Semantics for Effects with Guarded Interaction Trees' received a Distinguished Paper Award at POPL 2024.
- PhD, KU Leuven, 2018
- MSc, TU Dresden, 2013
He teaches courses such as Compilation, Program Logics, and Advanced Topics in Programming Language Theory. He collaborates extensively with researchers like Lars Birkedal, Robbert Krebbers, and Derek Dreyer, and mentors students in formal methods and PL theory.
