Zaawansowane programowanie funkcyjne
Część wykładu Zaawansowane programowanie funkcyjne dotycząca Coqa i Idrisa. 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. Język Idris jest funkcyjnym językiem programowania z typami zależnymi.
