System wspomagania dowodzenia Coq 1000-2M05DC

Dowody matematyczne sprawiają adeptom matematyki i informatyki dwa rodzaje trudności: po pierwsze trudno jest wpaść na to jak udowodnić dane twierdzenie, po drugie często trudno jest przekonać się, że napisany dowód jest kompletny i poprawny. W obu tych czynnościach, a szczególnie w weryfikacji, pomóc nam może komputer.

Proponujemy wykład monograficzny poświęcony systemowi wspomagania dowodzenia Coq. Celem wykładu jest przybliżenie zarówno praktycznych aspektów systemu, jak i jego podstaw teoretycznych. Pokażemy jak tworzyć i weryfikować dowody matematyczne, jak dowodzić poprawność programów, jak z gotowego dowodu wyekstrahować działający program w języku funkcyjnym, Wytłumaczymy co to jest izomorfizm Curry'ego Howarda, dlaczego rachunek konstrukcji jest logicznie niesprzeczny i co można zdefiniować za pomocą typów indukcyjnych.

Plan wykładu jest następujący:

1. Wprowadzenie do systemu Coq
Rola Coqa: weryfikacja dowodów, tworzenie dowodów, automatyzacja. Podstawy logiczne: Rachunek Konstrukcji, izomorfizm Curry'ego Howarda

2. Język matematyczny używany w Coqu
Język rachunku konstrukcji, definicje i aksjomaty, typy indukcyjne.

3. Tworzenie dowodów, czyli taktyki
Podstawowe taktyki, składanie taktyk, fazy tworzenia dowodu.

4. Dowodzenie własności programów
Programy funkcyjne zapisane w Coqu, specyfikacje, dowody.
Dowodzenie poprawności programów imperatywnych: rozszerzenia Why, Ktakatoa, Caduceus.

5. Automatyzacja czyli język taktyk
Taktyki automatyczne. Język Ltac - główne konstrukcje.

6. Logiczne podstawy systemu Coq
Własności rachunku konstrukcji: konfluencja, silna normalizacja, niesprzeczność logiczna.
Rozszerzenia rachunku konstrukcji: typy indukcyjne, typy koindukcyjne i hierarchię uniwersów.

7. Pozostałe mechanizmy systemu Coq
Mechanizm sekcji: zagnieżdżone konteksty i zasada abstrakcji.
Mechanizm modułów: moduły podstawowe, sygnatury, funktory.

Do tego wykładu przewidziane jest laboratorium z systemu Coq. Na zaliczenie przewidziane jest wykonanie małego projektu w grupach, który ewentualnie, o ile jakość jego wykonania na to pozwoli, będzie mógł zostać dołączony do biblioteki standardowej Coqa.

Trochę więcej informacji na temat tego wykładu i laboratorium można znaleźć pod adresem http://www.mimuw.edu.pl/~chrzaszcz/coq