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

Ведущий специалист: Илья Сергей, IMDEA Software Institute, Мадрид, Испания.

Аннотация школы:

Что такое доказательство математически строгого утверждения? Когда доказательство математического факта считается «убедительным»? Наконец, какие утверждения можно считать истинными?

Подобные вопросы оставим философам. Программисты же обычно решают практические проблемы:

Как эффективно написать программу по данной спецификации? Как понять, удовлетворяет ли код требованиям или нет? Наконец, какие спецификации программ являются выполнимыми? … oh wait.

В рамках данного курса мы рассмотрим фундаментальное соответствие между программами и доказательствами и выясним, что доказывать теоремы — так же увлекательно, как писать программы.

А кроме этого:

• познакомимся с системой интерактивных доказательств Coq и ее расширением Ssreflect;
• узнаем, чем конструктивная логика отличается от классической, и почему последняя ближе программистам по духу;
• разберемся с доказательствами по индукции и коиндукции, а также построением (ко)рекурсивных программ;
• встретим старых знакомых из курсов алгебры и дискретного анализа;
• вспомним, какие бывают семантики программ, сформулируем и докажем ряд фактов о них;
• познаем азы магии условных переписываний.

ВНИМАНИЕ! Посещение данного курса может временно вызвать побочные эффекты:

• осознание неформальности Математики-как-мы-ее-понимали;
• фрустрацию от нетривиальности доказательств «тривиальных» фактов;
• неспособность остановиться и оставить теорему недоказанной;
• пересмотр своего отношения к программированию и математике.

Требования к участникам: знание любого статически типизированного функционального языка (Haskell, OCaml, Standard ML, Scala, F#).