Niezawodność oprogramowania należy do najbardziej istotnych wyzwań
współczesnej informatyki. Systemy wspomagające dowodzenie twierdzeń, takie jak
[Coq](https://coq.inria.fr/), zyskują w ostatnich latach ogromną popularność
jako platformy wspierające konstruowanie poprawnego i bezpiecznego
oprogramowania, łącząc w sobie język programowania oraz system logiczny. Coq
pozwala nie tylko na formalne specyfikowanie oraz weryfikowanie poprawności
programów komputerowych (tzw. certyfikowanie kodu), ale także na precyzyjne
definiowanie i analizę całych języków programowania.
Przedmiot stanowi wprowadzenie do formalnych podstaw niezawodnego
oprogramowania przy użyciu systemu Coq. Poruszana tematyka dotyczy wybranych
elementów logiki, teorii języków programowania oraz samego systemu Coq, a
całość przedmiotu realizowana jest w oparciu o podręcznik [Software
Foundations](https://softwarefoundations.cis.upenn.edu).
Omawiane zagadnienia:
1. Programowanie funkcyjne w systemie Coq
2. Wnioskowanie w systemie Coq (definicje indukcyjne, dedukcja naturalna, język taktyk, automatyzacja wnioskowania)
3. Dowody jako programy (izomorfizm Curry'ego-Howarda, typy zależne, ekstrakcja programów z dowodów)
4. Semantyka operacyjna języków imperatywnych (strukturalna semantyka operacyjna małych i dużych kroków, maszyny abstrakcyjne, transformacje programów)
5. Specyfikacja i weryfikacja programów imperatywnych (logika Hoare'a)
6. Rachunek lambda z typami prostymi (semantyka operacyjna, sprawdzanie typu, normalizacja)
7. Rozszerzenia systemu typów prostych (rekordy i podtypowanie, modyfikowalny stan)
8. Losowe testowanie programów i specyfikacji (QuickChick)
Literatura:
1. Benjamin C. Pierce: [Software Foundations](https://softwarefoundations.cis.upenn.edu).
2. Benjamin C. Pierce: [Programming Languages and Types](https://www.cis.upenn.edu/~bcpierce/tapl/). The MIT Press, 2002
Wykładowcy: Małgorzata Biernacka i Dariusz Biernacki
