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 | Zadanie |
| 2. | $\lambda$-kalkul: Churchove kódovanie, Rekurzia | $\lambda$-kalkul, Churchove kódovanie | - | 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 | 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. | Curry-Howardova korešpondencia | - | - | - |
| 12. | - | - | - | - |
| 13. | - | - | - | - |