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
Förkunskaper
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