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

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 nivå 2 eller motsvarande från ett erkänt internationellt test, t.ex. TOEFL, IELTS.

Rekommenderade förkunskaper: uh

Alla tillfällen (1)

Liknande utbildningar

• TypteoriUniversitet/högskola
• Funktionell programmeringUniversitet/högskola
• Introduktion till funktionell programmeringUniversitet/högskola
• Introduktion till programmeringUniversitet/högskola