W ciągu ostatnich 30 lat rozwoju informatyki pojawiło się wiele narzędzi
umożliwiających formalizację i mechaniczną (a dla pewnych klas problemów
automatyczną) weryfikację twierdzeń dotyczących zarówno teorii matematycznych,
jak i np. programów komputerowych. Jednym z powszechnie używanych obecnie
systemów wspomagających dowodzenie twierdzeń jest system Coq
(<http://coq.inria.fr/>), oparty na rachunku konstrukcji z definicjami
indukcyjnymi. Coq pozwala na definiowanie funkcji (w stylu podobnym do języka
Caml) i predykatów, wyrażanie twierdzeń matematycznych i specyfikacji
oprogramowania, a także na interakcyjne przeprowadzanie formalnych,
weryfikowanych przez system dowodów takich twierdzeń oraz generowanie
certyfikowanego kodu. Celem wykładu jest zapoznanie studentów zarówno z
podstawami teoretycznymi rachunku konstrukcji, jak i praktycznym
wykorzystaniem narzędzi takich jak Coq do formalizacji i weryfikacji zagadnień
z różnych dziedzin matematyki i informatyki, ze szczególnym uwzględnieniem
metateorii języków programowania. Omówimy również izomorfizm Curry'ego-Howarda
i mechanizm generowania certyfikowanego kodu.
**Program:** **Wymagania:** Logika dla informatyków Programowanie
