An Introduction to Iris: Higher-Order Concurrent Separation Logic
- document 1 document 2 document 3
- niveau 1 niveau 2 niveau 3
- audio 1 audio 2 audio 3
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.