Исследовательская группа
Лаборатория языковых инструментов
Iris, a Modern Concurrent Separation Logic
27 сентября
Этот доклад посвящён фреймворку для доказательства многопоточных программ Iris, связанные с которым работы последние несколько лет регулярно встречаются на ICFP, POPL и PLDI. Мы рассмотрим проблемы, с которыми сталкивается такой фреймворк, и концепцию "коммутативные моноиды как ресурсы, инварианты как глобальное состояние", лежащую в основе Iris; посмотрим на небольшие примеры доказательств. От слушателя ожидается знакомство с тройками Хоара и понятием separation logic.
https://iris-project.org/
Язык встречи: английский
Ссылка на встречу: https://meet.google.com/myu-dhmz-gvu