Programowanie z typami zależnymi i dowodzenie twierdzeń

Typy w językach programowania służą gwarantowaniu własności programów. Używając typów zależnych możemy formułować bardziej precyzyjne własności i uzyskiwać silniejsze gwarancje. System Coq umożliwia programowanie funkcyjne z typami zależnymi wraz z możliwością automatycznego lub interaktywnego dowodzenia własności programów oraz ich ekstrakcją do języków takich jak Ocaml, Haskell, Scheme. Przedmiot ten ma na celu naukę systemu Coq głównie w oparciu o przykłady z dziedziny programowania.