Zoznam všetkých cieľov

Prednášky

Cvičenia

1. týždeň: Netypovaný jazyk NBL

1. Syntaktická analýza termov
2. Overenie syntaktickej korektnosti termov
3. Vlastnosti termov
4. Vyhodnotenie termov

2. týždeň: $\lambda$-kalkul, Churchove kódovanie

1. Syntaktická analýza termov
2. Voľné a viazané premenné
3. Vyhodnotenie termov $\beta,\alpha,\eta-redukcia$
4. Churchove kódovanie

3. týždeň: Rekurzia v netypovanom $\lambda$-kalkule

1. Rekurzia v $\lambda$ -kalkule

4. týždeň: Typovaný NBL a Jednoducho typovaný $\lambda$-kalkul

1. Typovaný NBL
2. Jednoducho typovaný $\lambda$ -kalkul

5. týždeň: Väzba let a súčinové typy

1. Odvodené tvary termov - väzba let
2. Binárny súčinový typ - dvojica
3. Súčinový typ $n$ -typov - $n$-tica
4. Súčinový typ $n$ -typov s pomenovanými návesťami - Záznam

6. týždeň: Súčtové typy

1. Binárny súčtový typ
2. Typ variant
3. Enumeračný typ
4. Typ voliteľné hodnoty (Options)

7. týždeň: Rekurzia a Zoznamy

1. Rekurzívne funkcie v typovanom $\lambda$ -kalkule
2. Zoznamy

8. týždeň: Rekurzívne typy

1. Rekurzívny typ: Prirodzené čísla
2. Rekurzívny typ: Zoznam
3. Rekurzívny typ: Binárny vyhľadávací strom

9. týždeň: Odvodenie typu

1. Odvodenie typu

10. týždeň: Let polymorfizmus a Systém F

1. Let polymorfizmus
2. Systém F

Interaktívny dokazovací systém Coq

1. týždeň: Úvod do funkcionálneho programovania v Coq

1. Oboznámenie sa a inštalácia interaktívneho dokazovacieho systému Coq
2. Naštudovanie základnej syntaxe a pochopenie základných princípov funkcionálneho programovania.
3. Programovanie v Coq

2. týždeň: Formálne dôkazy a jazyk Ltack

1. Vypracovať cvičenie

Zadania