IK3620 Typer, semantik och programmeringsspråk 7,5 hp

Types, Semantics, and Programming Languages

I denna kurs kommer du att lära dig grundläggande programspråksteori, inklusive formell semantik, typsystem och typsundhetsbevis. Kursen innehåller både teori och praktik. Under kursens gång kommer du även att implementera en programtolk för ett typat funktionellt språk, samt även lösa olika teoretiska övningar.

  • Utbildningsnivå

    Forskarnivå
  • Huvudområde

  • Betygsskala

    P, F

Det finns inget planerat kurstillfälle.

Lärandemål

Efter kursen kommer studenten kunna:
- Konstruera typsundhetsbevis
- Analysera typregler
- Analysera småstegs- och storstegs-operationell semantik
- Implementera en programtolk och en typkontrollerare för ett typbaserat funktionellt språk
- Tillämpa otypad och enkelt typad lambdakalkyl med utökningar

Kursens huvudsakliga innehåll

Kursen är uppdelad i tre separata moduler som täcker olika aspekter av typer, semantik och programspråksteori:
1. Operationell semantik och lambdakalkylen
   - Småstegs- och storstegs-operationell semantik
   - Otypad lambdakalkylen
   - Grundläggande typad funktionell programmering
2. Typad lambdakalkyl med utökningar
   - Typregler
   - Typsundhetsbevis
   - Semantik för let-bindning, par, tupler, records, sums, och listor
   - Referenser och undantag
3. Subtypning och polymorfism
   - Subtypspolymorfism
   - Parametrisk polymorfism
   - Ad-hoc polymorfism
   - Strukturella och nominella typsystem
   - Gradvis typning

Kursupplägg

Kursen består av ett antal seminarier. Under seminarierna presenterar studenterna lösningar till övningar och problem. Studenterna kommer att lösa både teoretiska problem samt implementera en fungerande programtolk och typkontrollerare för ett funktionellt programmeringsspråk.

Behörighet

Rekommenderade förkunskaper

Goda kunskaper inom programmering. God grundläggande förståelse av diskret matematik och logik.
Kunskap inom funktionell programmering och kompilatorer är en fördel men inte ett krav.

Litteratur

- Benjamin C. Pierce, "Types and Programming Languages", The MIT Press, 2002
- Selected research articles

Utrustningskrav

Varje student behöver en egen laptop.

Examination

  • EXA1 - Examination, 7,5, betygsskala: P, F

Se "Krav för slutbetyg" nedan.

Krav för slutbetyg

Studenten erhåller betyg P på kursen om följande är uppfyllt:
1. Aktivt deltagande i seminarier
2. Godkända muntliga presentationer vid seminarier
3. Godkända lösningar på teoretiska övningar
4. Godkänd inlämning och presentation av programvaruimplementation
Om studenten inte kan medverka på någon av seminarierna kan detta kompletteras vid ett alternativt tillfälle.

Ges av

EECS/Programvaruteknik och datorsystem

Examinator

David Broman <dbro@kth.se>

Versionsinformation

Kursplan gäller från och med VT2016.
Examinationsinformation gäller från och med VT2019.