About this event
Lars Birkedal
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 mathematical reasoning about safety and correctness of concurrent higher-order imperative programs.
More information: https://iww.inria.fr/colloquium/
Hosted by
