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](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 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)
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.
