Konspekt Baasväärtused ja tüübid 𝜆-arvutus Kõrgemat järku funktsioonid Interaktiivne programmeerimine Uute tüüpide loomine Liidesed Sisend-Väljund Laiskus Lihtsalt tüübitud 𝜆-arvutus Tüübituletus Sõltuvad tüübid Tõestamine Idrises Kvantitatiivne tüübiteooria
