Conférence
An Introduction to Iris: Higher-Order Concurrent Separation Logic
Durée : 01:01:24
-Réalisation : 23 septembre 2021
-Mise en ligne : 8 mars 2022
- document 1 document 2 document 3
- niveau 1 niveau 2 niveau 3
- audio 1 audio 2 audio 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.
Thème
Notice
Lieu de réalisation
Inria Sophia Antipolis Méditerranée
Langue :
Anglais
Crédits
Lars Birkedal (Intervenant)
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 29 septembre 2023)