Следить за анонсами можно в группе в Telegram.
По средам в 17:15, здание факультета математики и компьютерных наук СПбГУ, 14-я линия В.О., 29, аудитория 303. (внимание, в весеннем семестре время и место может измениться, следите за анонсами в Telegram-группе).
Формальная математическая семантика (спецификация) языка программирования позволяет строго рассуждать о поведении программ, написанных на данном языке, доказывать свойства самого языка программирования, таких как, например, безопасность его системы типов (typesafety), находить ошибки в дизайне языка и реализации его компилятора/интерпретатора. Кроме того наличие формальной семантики необходимо для последующей разработки инструментов верификации и поиска ошибок в программах (строго говоря, без наличия спецификации не совсем понятно, что вообще считать ошибкой, а что корректным поведением программы).
В рамках данного семинара мы обсуждаем вопросы определения формальной математической семантики параллельных, многопоточных и распределенных программ, систем и языков программирования. Особое внимание уделяется так называемым семантикам истинной конкурентности (true concurrency), и, в частности, структурам событий (event structures). Данный класс семантик позволяет явно задать причинно-следственные связи между атомарными событиями системы и не рассматривать все возможные чередования параллельных процессов. Такой подход позволяет упростить рассуждение о поведении параллельных программ, а также находит применение при разработке инструментов верификации.
Материал курса основан на книгах и статьях, приведенных по ссылке.
Семинар проходит в формате лекций, семинаров с разбором статей и (по желанию) докладов от участников. Также, материал лекций частично механизирован в системе доказательства теорем Coq.
Кому может быть интересно: интересующимся языками программирования и моделями вычислений; формальной верификацией; параллельными, многопоточными и распределенными системами.