Przedmiot stanowi wprowadzenie do podstaw językow programowania przy użyciu
systemu wspomagającego dowodzenie twierdzeń Coq, jak i do samego systemu.
Omawiane zagadnienia:
1. Programowanie funkcyjne w systemie Coq
2. Wnioskowanie w systemie Coq
3. Dowody jako programy
4. Semantyka językow imperatywnych (parsowanie, semantyka operacyjna, ewaluacja częściowa, logika Hoare'a)
5. Rachunek lambda z typami prostymi (normalizacja, sprawdzanie typu, modyfikowalny stan, rekordy, podtypowanie)
Literatura:
1. [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/). Benjamin C. Pierce. 2013
2. Programming Languages and Types. Benjamin C. Pierce. The MIT Press, 2002.
