Gå till huvudinnehåll

Typer för program och bevis

7.5 hp, Fristående kurs, Göteborgs universitet

Utbildningsområde: Metoder och beslutsstöd

Typ av utbildning:

Fristående kurs

Nivå:

Avancerad

Studieform:

Campus

Studietakt:

50%

Utbildningsort:

Göteborg

Undervisningstid:

Dag

Omfattning:

7.5 hp

Undervisningsspråk:

Engelska

Kursen startar:

2025-09-01

Sista dag för anmälan:

2025-04-15

Uppgifter om utbildningen hämtas från SUSA-navet som motsvarar innehållet på antagning.se Länk till annan webbplats, öppnas i nytt fönster..

Mer 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

Startperiod

HT-25

Startvecka

Vecka 36 2025

Slutvecka

Vecka 44 2025

Behörighetskrav

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.

Anmälningskod

86034

Kurskod

DIT235

Lärosäte som anordnar kursen

Göteborgs universitets vision Ett universitet för världen uttrycker universitetets strävan att vara ett internationellt lärosäte som tar ansvar för samhällsutvecklingen och bidrar till en hållbar värld. Visionen fastställer också att universitetets verksamhet vilar på de akademiska kärnvärden som formulerats i Universitetens Magna Charta och att dessa hålls levande inom ramen för den statliga värdegrunden.

Läs mer om Göteborgs universitet

Göteborgs universitet