Лаборатория языковых инструментов

Этот доклад посвящён фреймворку для доказательства многопоточных программ Iris, связанные с которым работы последние несколько лет регулярно встречаются на ICFP, POPL и PLDI. Мы рассмотрим проблемы, с которыми сталкивается такой фреймворк, и концепцию "коммутативные моноиды как ресурсы, инварианты как глобальное состояние", лежащую в основе Iris; посмотрим на небольшие примеры доказательств. От слушателя ожидается знакомство с тройками Хоара и понятием separation logic.

https://iris-project.org/

Язык встречи: английский

Ссылка на встречу: https://meet.google.com/myu-dhmz-gvu