Typer för program och bevis
Om utbildningen
Kraftfulla och flexibla typsystem är en viktig aspekt för moderna programmeringsspråk. Denna kurs ger en introduktion till detta område. Bland annat introducerar vi begreppet "beroende typ", dvs. en typ som kan bero på värden av en annan typ.
Beroende typer har många användningsområden. Genom att identifiera påståenden och typer (Curry-Howard identifieringen) kan man uttrycka i stort sett vilken egenskap som helst hos ett program. I kursen får studenten lära sig använda ett interaktivt programmeringssystem för beroende typer.
Kursen ska ge breda och gedigna kunskaper om hur typsystem för programspråk är uppbyggda, och dessutom ge exempel på typbaserade tekniker inom datavetenskapen.
- introduktion till lambdakalkyl och enkel typteori
- introduktion till operationell semantik och typsystem
- beroende typer
- Curry-Howard-identifieringen av påståenden och typer
- programmering i Agda, en bevisassistent
- presentation av avancerade ämnen inom typsystemområdet
Behörigheter och urval
Behörighet
För tillträde till kursen krävs att studenten har minst 120 hp i datavetenskap eller matematik, eller motsvarande. Specifikt krävs en 7,5 hp kurs i diskret matematik (t.ex. DIT980 Diskret matematik för Datavetare, eller motsvarande) och en 7,5 hp kurs i funktionell programmering (t.ex. DIT143 Funktionell programmering, eller motsvarande).
Följande kunskapsnivå i Engelska krävs; Engelska 6/Engelska B eller motsvarande från ett erkänt internationellt test, t.ex. TOEFL, IELTS.
Urval
Högskolepoäng, max 285 hp.
