Abstract

Modern programming languages such as Java, Scala, and Rust are examples of concurrent higher-order imperative programming languages.

In this talk I will give an introduction to our research on Iris, a logical framework, implemented and verified in the Coq proof assistant, which can be used for reasoning about safety of concurrent higher-order imperative programs and for reasoning about type systems, data-abstraction, etc.

Honorary Lecture

Lars Birkedal’s talk is the first out of three lectures in honor of three distinguished professors at the Department of Computer Science. After the talk, there will be a small reception outside the auditorium.

In 2017, Lars Birkedal were named Fellow by the Association for Computing Machinery (ACM) for his contributions to the semantic and logical foundations of compilers and program verification systems. ACM Fellow is the highest recognition given by the organization, and only 1% of the 100,000 members have reached this member grade.