Conférence
Notice
Lieu de réalisation
Inria Sophia Antipolis Méditerranée
Langue :
Anglais
Crédits
Lars Birkedal (Intervention)
Détenteur des droits
Inria
Conditions d'utilisation
Droit commun de la propriété intellectuelle
Citer cette ressource :
Lars Birkedal. Inria. (2021, 23 septembre). An Introduction to Iris: Higher-Order Concurrent Separation Logic. [Vidéo]. Canal-U. https://www.canal-u.tv/114724. (Consultée le 2 juin 2024)
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.