Conférence

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
  • 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.

Intervenants
Thèmes
Notice
Contacter

Sur le même thème