Typer för program och bevis

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 beoende 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