Typteori

Om utbildningen

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.

Behörighet

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

Rekommenderade förkunskaper: uh

Alla tillfällen (1)

Liknande utbildningar

• Typer för program och bevisUniversitet/högskola
• Grundläggande logik och modellteoriUniversitet/högskola
• Matematisk logik för datavetenskapUniversitet/högskola
• ProgrammeringsteoriUniversitet/högskola