Sök utbildning 👉
Fristående kurser (avancerad nivå)

Typteori

Stockholms universitet, i Stockholm
Längd
7.5 hp
Utbildningstakt
Deltid
Nästa startdatum
Vår 2025 se detaljer
Utbildningsform
Klassrum
Längd
7.5 hp
Utbildningstakt
Deltid
Nästa startdatum
Vår 2025 se detaljer
Utbildningsform
Klassrum

Typteori

Kursen ger en introduktion till typteori med enkla och beroende typer, och hur den kan användas för att representera logiska system och bevis, samt hur dess bevis ger upphov till beräkningsbara funktioner. I den avslutande delen tas tillämpningar av typteori upp.Typteori: Lambda-kalkyl, kontext, omdömen, enkla typer, induktiva typer. Operationell semantik: konfluens och normalisering. Curry-Howard-isomorfin. Martin-Löfs typteori: beroende typer, introduktions- och eliminationsregler, likhetstyper, universa. Brouwer- Heyting-Kolmogorov-tolkningen av logik. Meningsförklaringar. Semantik för beroende typer. Explicit substitution. Kategoriteoretiska modeller. Någon eller några av följande tillämpningsområden av typteori behandlas: homotopiteori, modeller för (konstruktiv) mängdteori och bevisassistenter.

Kommande starter

1 tillgängligt startdatum

Vår 2025

  • Klassrum
  • Stockholm

Förkunskaper

För tillträde till kursen krävs kunskaper motsvarande 90 högskolepoäng i matematik, inkluderande Logik (MM7008). Engelska B eller motsvarande.
Stockholms universitet

Stockholms universitet

En utbildning från Stockholms universitet är en merit som skapar goda förutsättningar för arbete och karriär, både nationellt och internationellt. Du kan välja bland över 200 program och 1900 fristående kurser inom humaniora, juridik, lärarutbildning, naturvetenskap, samhällsvetenskap och språk. Vid...

Läs mer om Stockholms universitet och visa alla utbildningar

Highlights