Loengud
NB! Video kiiruse muutmiseks võib olla vaja avada see siit!
| # | kuupäev | sisu | materjalid |
|---|---|---|---|
| 1 | 01.09 | sissejuhatus; ülevaade keelest Idris | video, loeng1.pdf, loeng1.idr |
| 2 | 08.09 | paradigmad; baasväärtused ja -tüübid | video, loeng2.pdf, loeng2.idr |
| 3 | 15.09 | {$\lambda$}-arvutus; kõrgemat järku funktsioonid | video, loeng3.pdf, loeng3.idr |
| 4 | 22.09 | reduktsioon; uute tüüpide loomine; kirjed | video, loeng4.pdf, loeng4.idr |
| 5 | 29.09 | reduktsiooni jrk, tüübiklassid, sisend-väljund | video, loeng5.pdf, loeng5.idr |
| 6 | 06.10 | {$\lambda$}-termidega arvutamine, seisundimonaad | video, loeng6.pdf, loeng6.idr |
| 7 | 13.10 | kordamine: reduktsioon, monaadid; püsipunktid | video, loeng7.pdf, loeng7.idr, StateT.idr |
| 8 | 20.10 | monaadidest maalähedaselt | video, loeng8.pdf, loeng8.idr |
| 9 | 27.10 | Lihtsalt tüübitud {$\lambda$}-arvutus | video, loeng9.pdf, loeng9.idr |
| 10 | 03.11 | Sõltuvad tüübid, Curry-Howard'i vastavus | video, loeng11.pdf, loeng10.idr |
| 11 | 10.11 | Curry-Howard'i vastavus (jätk) | video, loeng11.pdf, loeng11.idr |
| 12 | 17.11 | kvantitatiivne tüübiteooria | video, loeng12.idr |
| 13 | 24.11 | tüübituletus | video, loeng13.pdf |
| 14 | 01.12 | (ei toimu) | |
| 15 | 08.12 | Laiskus, Kategooriad | video, loeng14.pdf, Loeng14.hs |
| 16 | 15.12 | Kategooriad, Laiskus (jätk) | video, loeng14.pdf, loeng15.idr |
Praktikumid
| # | kuupäev | sisu | kodutöö tähtaeg |
|---|---|---|---|
| 0 | - | Kodus: Idris2 ja VS Code installimine | |
| 1 | 06.09 | Rekursiivsed funktsioonid täisarvudel | Kodutöö 1 (P1): 13.09 |
| 2 | 13.09 | Listifunktsioonid | Kodutöö 2 (P2): 20.09 |
| 3 | 20.09 | Kõrgemat järku funktsioonid | Kodutöö 3 (P3): 27.09 |
| 4 | 27.09 | Andmestruktuurid ja kirjed | Kodutöö 4 (P4): 04.10 |
| 5 | 04.10 | Tüübiklassid, sisend-väljund | Kodutöö 5 (P5): 11.10 |
| 6 | 11.10 | Reduktsioon {$\lambda$}-arvutuses | Kodutöö 6 (P6): 25.10 |
| 7 | 18.10 | Konsultatsioon | |
| 8 | 25.10 | Vahekontrolltöö! | |
| 9 | 01.11 | Monaadid ja tüüpimispuud | Kodutöö 7 (P9): 8.11 |
| 10 | 08.11 | Sõltuvate tüüpidega programmeerimine | Kodutöö 8 (P10): 15.11 |
| 11 | 15.11 | Tõestamine | Kodutöö 9 (P11): 22.11 |
| 12 | 22.11 | Lineaarsed tüübid | Kodutöö 10 (P12): 29.11 |
| 13 | 29.11 | 2. kontroltöö küsimuste harjutamine | |
| 14 | 06.12 | Projektid, Konsultatsioon | |
| 15 | 13.12 | Kontrolltöö! |