Stockholms universitet logo, länk till startsida
Go to this page on our english site

Typteori

Typteori ges på engelska och du hittar mer information om kursen på den engelska versionen av denna sida - klicka på det lilla jordklotet till höger om kursnamnet.

Du hittar även den engelska versionen av sidan här

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.