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. Definovať a vyhodnotiť rekurzívne funkcie v $\lambda$ -kalkule pomocou Churchovho kódovania a Curryho kombinátora $Y$ .

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 Rocq Prover

1. týždeň: Úvod do funkcionálneho programovania v Rocq a prvé dôkazy

1. spustiť Rocq, pracovať v RocqIDE a rozlíšiť term Galliny, príkaz Vernacular a taktiku;
2. pomocou Definition , fun , Check , Compute a Print definovať a skúmať funkcie a ich typy;
3. definovať induktívny typ, spracovať ho pomocou match , napísať jednoduchý Fixpoint a vysvetliť úplnosť vzorov a kontrolu terminácie.
4. sledovať dôkazový stav a zostaviť jednoduché dôkazy pomocou základných taktík.

2. týždeň: Dôkaz indukciou a funkcie vyššieho rádu

1. Indukcia nad prirodzenými číslami a dôkazové stavy
2. Taktiky exact , apply , rewrite , assert a replace
3. Formálny a neformálny dôkaz; rozdiel medzi bool a Prop
4. Funkcie vyššieho rádu: filter , map a fold_right
5. Samostatné úlohy k dôkazom a funkciám vyššieho rádu

3. týždeň: Údajové štruktúry a polymorfizmus

1. Údajové štruktúry: dvojica a zoznam
2. Logické uvažovanie o dvojiciach a zoznamoch
3. Typ option pre čiastočne definované funkcie
4. Polymorfné verzie dvojice, zoznamu a typu option

Zadania