Prehľad predmetu

Týždeň	Prednášky	Cvičenia	Interaktívny dokazovací systém Coq	Zadania
1.	Úvod, jazyk NBL, $\lambda$-kalkul	Netypovaný jazyk NBL	Úvod do funkcionálneho programovania v Coq	Zadanie
2.	$\lambda$-kalkul: Churchove kódovanie, Rekurzia	$\lambda$-kalkul, Churchove kódovanie	Formálne dôkazy a jazyk Ltack	Užitočné odkazy
3.	Typovaný NBL, Jednoducho typovaný $\lambda$-kalkul	Rekurzia v netypovanom $\lambda$-kalkule	-	-
4.	Jednotkový typ, Odvodené tvary termov, Súčinové typy	Typovaný NBL a Jednoducho typovaný $\lambda$-kalkul	-	-
5.	Súčtové typy, Curry-Howardova korešpondencia	Väzba let a súčinové typy	-	-
6.	Rekurzia v typovanom $\lambda$-kalkule, Zoznamy, Rekurzívne typy	Súčtové typy	-	-
7.	Odvodenie typu	Rekurzia a Zoznamy	-	-
8.	Systém F a Let polymorfizmus	Rekurzívne typy	-	-
9.	Systém $\lambda \underline{\omega}$	Odvodenie typu	-	-
10.	Systém $\lambda P$	Let polymorfizmus a Systém F	-	-
11.	Referenčné typy, Výnimočné situácie, Podtypy	-	-	-
12.	-	-	-	-
13.	-	-	-	-