Niezawodność oprogramowania należy do najbardziej istotnych wyzwań współczesnej informatyki. Systemy wspomagające dowodzenie twierdzeń, takie jak [Rocq](https://rocq-prover.org) (dawniej Coq), 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. Rocq 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 Rocq. Poruszana tematyka dotyczy wybranych elementów logiki, teorii języków programowania oraz samego systemu Rocq, a całość przedmiotu realizowana jest w oparciu o podręcznik [Software Foundations](https://softwarefoundations.cis.upenn.edu).
Omawiane zagadnienia:
- programowanie funkcyjne w systemie Rocq
- wnioskowanie w systemie Rocq (definicje indukcyjne, dedukcja naturalna, język taktyk, automatyzacja wnioskowania)
- dowody jako programy (izomorfizm Curry’ego-Howarda, typy zależne, ekstrakcja programów z dowodów)
- semantyka operacyjna języków imperatywnych (strukturalna semantyka operacyjna małych i dużych kroków, maszyny abstrakcyjne, transformacje i optymalizacja programów)
- specyfikacja i weryfikacja programów imperatywnych (logika Hoare’a)
- rachunek lambda z typami prostymi (semantyka operacyjna, sprawdzanie typu, normalizacja)
- rozszerzenia systemu typów prostych (rekordy i podtypowanie, modyfikowalny stan)
Przedmiot został zaprojektowany jako łagodne wprowadzenie do interaktywnego dowodzenia twierdzeń o poprawności programów i systemów logicznych przy wykorzystaniu wiedzy z przedmiotów _Logika dla informatyków_, _Metody programowania_ oraz _Programowanie funkcyjne_, jednocześnie oferując przedsmak tego czego można nauczyć się na bardziej zaawansowanych przedmiotach dotyczących semantyki języków programowania, systemów typów czy weryfikacji programów.
Wykładowcy: Małgorzata Biernacka i Dariusz Biernacki
