Typteori
Stockholms universitetTypteori
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.
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...
Hitta till utbildaren
Stockholms universitet
Recensioner
Det finns inga recensioner för Typteori
Jobb & Lön
Var finns framtidens jobb & hur mycket kommer jag att tjäna?
Få koll på vad du kan tjäna efter din utbildning och om den branschen är värd att investera din tid i.
