Lars Birkedal – An Introduction to Iris: Higher-Order Concurrent Separation Logic
September 23rd, 2021 – 11:00 am 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…