Hoppa till huvudinnehåll
Länkstig

Typer för program och bevis

Kurs
Avancerad nivå
7,5 högskolepoäng (hp)
Studietakt
50%
Undervisningstid
Dag
Studieort
Göteborg
Undervisningsform
Campus
Undervisningsspråk
Engelska
Start/slut
-
Ansökan öppen
-
Anmälningskod
GU-18660
Ansökan stängd

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.

Behörigheter och urval

Förkunskapskrav

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 225 hp.

För antagning till sommaren 2021 och framåt gäller följande urval: högskolepoäng, max 165 hp.