Niezawodność oprogramowania należy do najbardziej istotnych wyzwań
wspoł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
programow komputerowych (tzw. certyfikowanie kodu), ale także na precyzyjne
definiowanie i analizę całych językow programowania.
Przedmiot stanowi wprowadzenie do formalnych podstaw niezawodnego
oprogramowania, przy użyciu systemu Coq. Poruszana tematyka dotyczy wybranych
elementow logiki, teorii językow programowania oraz samego systemu Coq, a
całość przedmiotu realizowana jest w oparciu o podręcznik [Software
Foundations](http://www.cis.upenn.edu/%7Ebcpierce/sf/current/index.html).
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 programow z dowodow)
4. Semantyka operacyjna językow imperatywnych (strukturalna semantyka operacyjna małych i dużych krokow, maszyny abstrakcyjne, transformacje programow)
5. Specyfikacja i weryfikacja programow imperatywnych (logika Hoare'a)
6. Rachunek lambda z typami prostymi (semantyka operacyjna, sprawdzanie typu, normalizacja)
Literatura:
1. Benjamin C. Pierce. [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/). 2015
2. Benjamin C. Pierce. [Programming Languages and Types](https://www.cis.upenn.edu/~bcpierce/tapl/). The MIT Press, 2002.
