Monday 16 September 2019, 14:00, LSV library: Prophecy Variables in Separation Logic, Rodolphe Lepigre (post-doc, MPI).

Je pense faire une introduction à Iris (la logique de séparation d'ordre supérieur développée par le groupe de Derek Dreyer) et aux « variables de prophétie » (qu'on a récemment intégré à Iris) pour pouvoir encoder des spécifications très fortes pour des structures de données concurrentes.