Kursplan för Typer för bevis och program

Kursplan fastställd 2021-02-26 av programansvarig (eller motsvarande).

Kursöversikt

  • Engelskt namnTypes for programs and proofs
  • KurskodDAT350
  • Omfattning7,5 Högskolepoäng
  • ÄgareMPALG
  • UtbildningsnivåAvancerad nivå
  • HuvudområdeDatateknik, Informationsteknik
  • InstitutionDATA- OCH INFORMATIONSTEKNIK
  • BetygsskalaTH - Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3), Underkänd

Kurstillfälle 1

  • Undervisningsspråk Engelska
  • Anmälningskod 02113
  • Blockschema
  • Sökbar för utbytesstudenterJa

Poängfördelning

0117 Muntlig tentamen 7,5 hp
Betygsskala: TH		7,5 hp

I program

Examinator

Gå till kurshemsidan (Öppnas i ny flik)

Behörighet

Grundläggande behörighet för avancerad nivå
Sökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.

Särskild behörighet

Engelska 6
Sökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.

Kursspecifika förkunskaper

120 hp i datavetenskap eller matematik eller motsvarande samt grundläggande kunskaper i logik och funktionell programmering.

Syfte

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.

Lärandemål (efter fullgjord kurs ska studenten kunna)

  • hur man programmerar i ett funktionellt programmeringsspråk med beroende typer
  • hur man bevisar teorem i ett funktionellt programmeringsspråk med beroende typer
  • förstå hur man använder deduktionssystem för att presentera typsystem och beräkningsregler för programmeringsspråk

Innehåll

  • Introduktion till operationell semantik och typsystem
  • Beroende typer
  • Curry-Howard identifieringen av påståenden och typer
  • Programmering i Agda, en bevisassistent
  • Presentation av forskningsartiklar om typsystem

Organisation

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

Litteratur

  • Types and Programming Languages by Benjamin Pierce, MIT Press
  • Verified Functional Programming in Agda by Aaron Stump, Association for Computing Machinery and Morgan & Claypool

Examination inklusive obligatoriska moment

  • Hemtentamen för betyg 3, utöver detta muntlig tentamen för betyg 4 eller 5
  • Presentation av avancerat ämne eller forskningsresultat om typsystem eller av programmeringsprojekt i det beroende typade språket Agda

Kursens examinator får examinera enstaka studenter på annat sätt än vad som anges ovan om särskilda skäl föreligger, till exempel om en student har ett beslut från Chalmers om pedagogiskt stöd på grund av funktionsnedsättning.