Лаборатория языковых инструментов
Программы и доказательства: автоматизация математики на основе зависимых типов
Ведущий специалист: Илья Сергей, IMDEA Software Institute, Мадрид, Испания.
Аннотация школы:
Что такое доказательство математически строгого утверждения? Когда доказательство математического факта считается «убедительным»? Наконец, какие утверждения можно считать истинными?
Подобные вопросы оставим философам. Программисты же обычно решают практические проблемы:
Как эффективно написать программу по данной спецификации? Как понять, удовлетворяет ли код требованиям или нет? Наконец, какие спецификации программ являются выполнимыми? … oh wait.
В рамках данного курса мы рассмотрим фундаментальное соответствие между программами и доказательствами и выясним, что доказывать теоремы — так же увлекательно, как писать программы.
А кроме этого:
- познакомимся с системой интерактивных доказательств Coq и ее расширением Ssreflect;
- узнаем, чем конструктивная логика отличается от классической, и почему последняя ближе программистам по духу;
- разберемся с доказательствами по индукции и коиндукции, а также построением (ко)рекурсивных программ;
- встретим старых знакомых из курсов алгебры и дискретного анализа;
- вспомним, какие бывают семантики программ, сформулируем и докажем ряд фактов о них;
- познаем азы магии условных переписываний.
ВНИМАНИЕ! Посещение данного курса может временно вызвать побочные эффекты:
- осознание неформальности Математики-как-мы-ее-понимали;
- фрустрацию от нетривиальности доказательств «тривиальных» фактов;
- неспособность остановиться и оставить теорему недоказанной;
- пересмотр своего отношения к программированию и математике.
Требования к участникам: знание любого статически типизированного функционального языка (Haskell, OCaml, Standard ML, Scala, F#).