Type theory

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.

Eligibility: The course Logic (MM7008) corresponds to the newer version Mathematics III - Logic (MM5024).

The course consists of one element.


Teaching Format

Teaching consists of lectures and exercise sessions.


Assessment

Assessment takes place through a written assignments, and written and oral exams.

Examiner

The schedule will be available no later than one month before the start of the course. We do not recommend print-outs as changes can occur. At the start of the course, your department will advise where you can find your schedule during the course.


Note that the course literature can be changed up to two months before the start of the course.

Per Martin-Löf: Intuitionistic Type Theory. Bibliopolis.

List of course literature Department of Mathematics

Course reports are displayed for the three most recent course instances.

New student
During your studies

Course web

You can find our course webpages on kurser.math.su.se.






Cookie settings

By allowing third-party services, you accept their cookies and the use of tracking technologies necessary for them to function properly.