An Introduction to Iris: Higher-Order Concurrent Separation Logic

This lecture by Lars Birkedal introduces Iris, a logical framework implemented in Coq for reasoning about safety and correctness of concurrent higher-order imperative programs. The talk covers the challenges of modeling and reasoning about modern programming languages, the use of Iris for program logics, and the application of Iris in defining and proving properties of programs. Lars Birkedal also discusses the importance of types in expressing invariants and the unique characteristics of Iris in formal Coq verification. The lecture delves into examples of Hoare triples, separation logic, operational semantics, and the application of Iris in program logics and type soundness. Lars Birkedal highlights the significance of Iris in logical relations for concurrent programming languages and its role in verifying complex programs.