Исследовательская группа

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

Программы и доказательства: автоматизация математики на основе зависимых типов

25-29 августа 2014 г.

5661b95175d86.jpg

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

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

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

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

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

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

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

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

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

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

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

Дополнительно