Seminar • Programming Languages • Formal Reasoning About Programs

Please note: This seminar will take place in DC 1304.

Amin Timany, Assistant Professor
Logic and Semantics Group, Department of Computer Science, Aarhus University

Nowadays, there is virtually no industry or any aspect of our personal lives that computer systems do not touch. This prevalence means that there is great potential for harm caused by incorrect, buggy implementations of software systems, especially in critical applications. However, correctly designing and implementing programs, especially concurrent and distributed programs, is notoriously difficult. Hence it is of paramount importance to analyze programs to eliminate bugs.

In this talk I will present my research in formal reasoning about programs using program logics. A program logic is a formal language based on mathematical logic for expressing and proving various properties of programs. State-of-the-art program logics have been extremely successful. They have been used in a wide range of applications from reasoning about correctness of type systems of high-level functional and imperative programming languages to hardware security guarantees in assembly languages. This talk will focus on the application of state-of-the-art program logics to reasoning about various aspects of correctness of concurrent and distributed programs.

Bio: Amin Timany is a tenure-track assistant professor in the Logic and Semantics research group of the Department of Computer Science of Aarhus University, Aarhus, Denmark. Before joining Aarhus University in April 2020, he was a postdoctoral fellow of the Flemish research fund (FWO) at the DistriNet research group of the Department of Computer Science of KU Leuven, Leuven, Belgium. Prior to that, Amin obtained his PhD in May 2018 from KU Leuven under supervision of Prof. Bart Jacobs.

Amin’s research interests include formal program verification, program logics, compilers, type theory, proof assistants, formalization of mathematics in proof assistants, and category theory. His research together with his collaborators has resulted in several publications in the very top international venues in the field of programming languages, most frequently (10 papers) in Principles of Programming Languages (POPL). Ever since the beginning of his postdoctoral fellowship Amin has supervised six PhD students and a postdoc — out of the six PhD students three have graduated two of whom have continued their careers as postdoctoral researchers, and one has joined the industry.