Семантика языков программирования

Когда мы пишем программы, мы не оперируем элементарными терминами языка программирования, подобно тому, как, говоря на родном языке, мы не размышляем в терминах синтаксиса и морфологии. Человеческое мышление мнемонично, оно действует в терминах абстракций и идиом. Такой способ рассуждений хорошо работает при создании прикладных программ, однако даёт странные и иногда необъяснимые результаты при реализации языковых инструментов, то есть программ, которые получают на вход одни программы и возвращают другие (компиляторов, интерпретаторов, специализаторов и т. д.).

Это происходит оттого, что такие инструменты должны правильно работать для всех исходных программ, а не только для таких, которые состоят из удобных нам мнемонических структур. Например, что следует делать, если в программе на языке C в теле цикла while мы встретили оператор case (сразу, без switch)?

Довольно быстро (после каких-то 20 лет развития науки о языках программирования) оказалось, что для надёжной работы таких инструментов (или, как минимум, для правдоподобного обоснования, почему они работают именно так) необходимы способы формальной и точной спецификации семантики языков программирования, которые предоставили бы средства для математического доказательства свойств программ и их преобразователей.

В рамках данного курса мы познакомимся со способами формального описания семантик языков программирования, которые позволяют всё это проделывать, а также научимся доказывать свойства программ и их преобразований, пользуясь инструментом для автоматизированного доказательства теорем Rocq.

Пререквизиты курса:

• знание какого-либо языка программирования (а лучше нескольких, а лучше — принадлежащих разным парадигамам (C — Java — Haskell и т.д.))
• начало мат. логики
• начало дискретного анализа