Type theory

Utbildningsfakta

Kod: MM8036

The course provides an introduction to type theory with simple and dependent types, how it can be used to represent logical systems and proofs, and how proofs give rise to computable functions. The final part of the course covers applications of type theory. The following topics are covered: Type theory: lambda calculus, contexts, forms of judgement, simple types, inductive types. Operational semantics: confluence and normalization. The Curry-Howard isomorphism. Martin-Löf type theory: dependent types, induction and elimination rules, identity types, universes. The Brouwer-Heyting-Kolmogorov interpretation of logic. Meaning explanations. Semantics of dependent types. Explicit substitution. Category theoretical models. One or more of the following areas of application of type theory are covered: homotopy theory, models for (constructive) set theory and proof assistants.

Behörighet

Admission to the course requires knowledge equivalent to at least 90 credits in mathematics, including the course Logic 7.5 credits (MM7008). English B/English 6 or equivalent.

Utbildningstillfällen

Varje tillfälle har egna datum och villkor. Avslutade tillfällen behålls som historik och innebär inte att en ny ansökan är öppen.

• Type theory

  Stockholm University

  Stockholm

  Startdatum: 18 januari 2027

  Slutdatum: 6 juni 2027

  Studietakt: 25 %