Typer för program och bevis

Kursen kan ingå i följande program:

1. Computer Science, mastersprogramme (N2COS)
2. Datavetenskap, kandidatprogram (N1COS)

Kursen ges även som fristående kurs vid Göteborgs Universitet.

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.

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

Efter godkänd kurs ska studenten kunna:

Kunskap och förståelse

• beskriva olika sorters typsystem, deras underliggande designprinciper, och deras semantiska grundvalar
• läsa och presentera ett forskningsämne inom området

Färdigheter och förmåga

• programmera i ett funktionellt programmeringsspråk med beroende typer
• bevisa teorem i ett funktionellt programmeringsspråk med beroende typer, med användning av principen "propositioner-som-påståenden"
• använda deduktionssystem för att presentera typsystem och beräkningsregler för programmeringsspråk

Värderingsförmåga och förhållningssätt

• kritiskt analysera typsystem och bevisa egenskaper hos dem

Undervisning ges i form av föreläsningar, övningar och handledning.

Undervisningsspråk: engelska

Kursen examineras genom en muntlig presentation som normalt genomförs i par, och en individuell hemtentamen. Dessutom, för att för ett högre betyg än 3 måste studenten godkännas på en muntlig individuell tentamen.

Hemtentamen inkluderar både teoretiska problem och programmeringsuppgifter. För den muntliga presentationen kan studenten antingen välja en forskningsartikel eller ett kapitel i kursboken som innehåller tillämpningar av typsystem som inte har täckts i föreläsningarna.

Om hemtentamen lämnas in försent så underkänns den. Omexamination av hemtentamen sker genom en individuell muntlig tentamen.

Om en student som har underkänts två gånger på samma examinerande moment önskar byta examinator inför nästa examinationstillfälle ska en sådan begäran bifallas om det inte finns särskilda skäl däremot (6 kap. 22 § HF).

Om en student har fått besked om pedagogiskt stöd från Göteborgs universitet med rekommendation om anpassad examination och/eller anpassad examinationsform kan examinator, i det fall det är förenligt med kursens lärandemål och förutsatt att inte orimliga resurser krävs, besluta att bevilja studenten anpassad examination och/eller anpassad examinationsform.

Om en kurs har avvecklats eller genomgått en större förändring ska studenten erbjudas minst två examinationstillfällen, utöver ordinarie examinationstillfälle. Dessa tillfällen fördelas under en tid av minst ett år, dock som längst två år efter det att kursen avvecklats/förändrats. Vad gäller praktik och verksamhetsförlagd utbildning (VFU) gäller motsvarande, men med begränsning till endast ett ytterligare examinationstillfälle.

Om en student har fått besked om att denne uppfyller kraven för att vara student vid Riksidrottsuniversitetet (RIU-student) har examinator rätt att besluta om anpassning vid examination, om detta görs i enlighet med Lokala regler gällande RIU-studenter vid Göteborgs universitet

Delkurser

1. Hemtentamen, 7,5 hp
   Betygsskala: Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U)

På kursen ges något av betygen Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U).

Betyget på kursen är detsamma som betyget på delkursen Hemtentamen.

Kursen utvärderas genom möten, både under och efter kursen, mellan lärare och studentrepresentanter. Ett anonymt skriftligt frågeformulär skickas även ut till studenterna efter kursens slut. Resultaten av utvärderingarna används för att förbättra kursinnehållet och som indikation till vilka delar som skulle kunna läggas till, tas bort, förbättras eller ändras.

Kännedom om funktionell programmering är rekommenderat, t.ex., från kursen DIT143 Funktionell programmering, eller motsvarande.

Kursen är samläst med Chalmers.

Kursen ersätter kursen DIT233, 7,5 hp. Den här kursen kan inte ingå i en examen som innehåller DIT233. Den kan inte heller ingå i en examen som bygger på en annan examen där DIT233 ingår.