Prehľad predmetu

Týždeň	Prednášky	Cvičenia	Interaktívny dokazovací systém Rocq Prover	Zadania
1.	Úvod, jazyk NBL, $\lambda$-kalkul	Netypovaný jazyk NBL	Úvod do funkcionálneho programovania v Rocq a prvé dôkazy	Zadanie
2.	λ-kalkul: Churchove kódovanie, rekurzia	$\lambda$-kalkul, Churchove kódovanie	Dôkaz indukciou a funkcie vyššieho rádu	Užitočné odkazy
3.	Typovaný NBL, Jednoducho typovaný $\lambda$-kalkul	Rekurzia v netypovanom $\lambda$-kalkule	Údajové štruktúry a polymorfizmus	-
4.	Jednotkový typ, Odvodené tvary termov, Súčinové typy	Typovaný NBL a Jednoducho typovaný $\lambda$-kalkul	Ďalšie taktiky a logika v Rocq	-
5.	Súčtové typy	Väzba let a súčinové typy	Induktívne definované výroky a jazyk NBL	-
6.	Rekurzia v typovanom $\lambda$-kalkule, Zoznamy, Rekurzívne typy	Súčtové typy	Zobrazenia a Jednoducho typovaný lambda kalkul	-
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.	Curry-Howardova korešpondencia	-	-	-
12.	-	-	-	-
13.	-	-	-	-