Conférence
Notice
Lieu de réalisation
Inria Sophia Antipolis Méditerranée
Langue :
Anglais
Crédits
Lars Birkedal (Intervention)
Crédit image : Inria Sophia Antipolis Méditerranée
Détenteur des droits
Inria Sophia Antipolis Méditerranée
Conditions d'utilisation
Droit commun de la propriété intellectuelle
DOI :
10.60527/fbae-hm62
Citer cette ressource :
Lars Birkedal. Inria. (2021, 23 septembre). An Introduction to Iris: Higher-Order Concurrent Separation Logic. [Vidéo]. Canal-U. https://doi.org/10.60527/fbae-hm62. (Consultée le 19 juillet 2025)
An Introduction to Iris: Higher-Order Concurrent Separation Logic
Réalisation : 23 septembre 2021
- Mise en ligne : 8 mars 2022
- document 1 document 2 document 3
- niveau 1 niveau 2 niveau 3
Descriptif
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.