Семантика языков программирования
⭐️ Лектор
Дмитрий Булычев
К.ф-м.н., с.н.с. междициплинарной лаборатории им. Чебышёва, руководитель магистратуры «Разработка ПО и науки о данных» МКН СПбГУ. Область научных интересов — языки и инструменты программирования, функциональное, логическое и реляционное программирование.
📢 Анонс
Когда мы пишем программы, мы не оперируем элементарными терминами языка программирования, подобно тому, как, говоря на родном языке, мы не размышляем в терминах синтаксиса и морфологии. Человеческое мышление мнемонично, оно действует в терминах абстракций и идиом. Такой способ рассуждений хорошо работает при создании прикладных программ, однако даёт странные и иногда необъяснимые результаты при реализации языковых инструментов, то есть программ, которые получают на вход одни программы и возвращают другие (компиляторов, интерпретаторов, специализаторов и т. д.).
Это происходит оттого, что такие инструменты должны правильно работать для всех исходных программ, а не только для таких, которые состоят из удобных нам мнемонических структур. Например, что следует делать, если в программе на языке C в теле цикла while мы встретили оператор case (сразу, без switch)?
Довольно быстро (после каких-то 20 лет развития науки о языках программирования) оказалось, что для надёжной работы таких инструментов (или, как минимум, для правдоподобного обоснования, почему они работают именно так) необходимы способы формальной и точной спецификации семантики языков программирования, которые предоставили бы средства для математического доказательства свойств программ и их преобразователей.
В рамках данного курса мы познакомимся со способами формального описания семантик языков программирования, которые позволяют всё это проделывать, а также научимся доказывать свойства программ и их преобразований, пользуясь инструментом для автоматизированного доказательства теорем Rocq.
📑 Пререквизиты курса
– знание какого-либо языка программирования (а лучше нескольких, а лучше — принадлежащих разным парадигамам (C — Java — Haskell и т.д.))
– начало мат. логики
– начало дискретного анализа
🕑 Курс будет проходить проходить по понедельникам с 18:00 в Мраморном зале, ПОМИ РАН, наб. реки Фонтанки, 27, Санкт-Петербург. Дату первой лекции сообщим позже. Записаться на курс можно через личный кабинет или в боте:
▶️ Личный кабинет
▶️ Бот