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

4. týždeň: Ďalšie taktiky

1. Používať taktiky na prácu s rovnosťami a spormi.
2. Upravovať kontext a pripravovať indukčné dôkazy.
3. Kombinovať taktiky pri riešení viacerých podcieľov.

5. týždeň: Logika v Rocq

1. Rozlišovať booleovské výpočty a tvrdenia v Prop .
2. Dokazovať tvrdenia s logickými spojkami a kvantifikátormi.
3. Rozlišovať konštruktívne a klasické dokazovanie.

6. týždeň: Induktívne definované výroky

1. Definovať predikáty pomocou induktívnych pravidiel.
2. Analyzovať dôkazy pomocou destruct a inversion .
3. Dokazovať vlastnosti relácií a ich uzáverov.

7. týždeň: Jazyk NBL

1. Formalizovať syntax, sémantiku a typy jazyka NBL.
2. Odvodzovať kroky vyhodnotenia a typové úsudky.
3. Dokazovať progres a zachovanie typu.

8. týždeň: Zobrazenia

1. Reprezentovať úplné a čiastočné zobrazenia pomocou funkcií.
2. Dokazovať vlastnosti vyhľadávania a aktualizácie.
3. Používať reflexiu a funkčnú extenzionalitu.

9. týždeň: Jednoducho typovaný λ-kalkul

1. Definovať syntax jednoducho typovaného lambda kalkulu.
2. Formalizovať substitúciu a sémantiku malých krokov.
3. Konštruovať typové odvodenia s typovým kontextom.

Ďalšie informácie