Master-Seminar: Type Theory (WiSe 2025/26)
Instructor: Massin Guerdi
Content
Type theory is the study of type systems, which form an important part of many programming languages. They are used to state and prove properties of programs (e.g. "this function produces an integer, when given a string"). In this sense they can be regarded as a kind of logic.
So called dependent type systems (also called "dependent type theories" or just "type theories") can be understood both as powerful logics and functional programming languages in their own right. They have been studied since the late 1960s and serve as the foundation of popular interactive theorem provers such as Agda, Rocq, Idris and Lean.
In this seminar, we will discuss various important type systems and their properties.
Prerequisites
- Familiarity with basic logic (propositional and first-order) is assumed.
- Familiarity with functional programming is helpful but not required.
Organisation
There will be some lectures at the start of the term, which will introduce the key concepts and notations of type theory. These lectures should give you the background knowledge required to understand type theory papers.
Afterwards, each student chooses a topic and prepares a written report and a talk about this topic. The topic is usually a paper about a particular type system, type-theoretic construction or proof method. Some suitable topics will be provided, but you can also suggest your own.
The talks will be given on one or more presentation days towards the end of the term, and the reports are due shortly thereafter.
Examination
You'll be graded on two products:
- A written report on your topic (60% of the grade). The report must be between 20,000 and 30,000 characters (~5-8 pages) long.
- A talk about your topic (40% of the grade) of 20-30 minutes plus 5-10 minutes discussion.
Attendance is mandatory at the first session and on the presentation days. Attendance at the other sessions is optional but highly recommended.
Chat
There's a chatroom for this seminar on the IFI Zulip chat: TCS-25W26-TT.
Schedule
There will be 5 weekly meetings, starting in the second week of the semester. The meetings take place on Mondays, 14:15-16:45, at Oettingenstraße 67, room L109.
See below for the exact schedule.
| Date | Topic | Room |
|---|---|---|
| 2025-10-20, 14-16 c.t. | lecture 1 | Oettingenstr. 67 L109 |
| 2025-10-27, 14-16 c.t. | lecture 2 | Oettingenstr. 67 L109 |
| 2025-11-03, 14-16 c.t. | lecture 3 | Oettingenstr. 67 L109 |
| 2025-11-10, 14-16 c.t. | lecture 4 | Oettingenstr. 67 L109 |
| 2025-11-17, 14-16 c.t. | lecture 5 | Oettingenstr. 67 L109 |
| TBD | student presentations | TBD |
| TBD | student presentations | TBD |
| TBD | student paper submissions |
Material
Course materials will be provided on Moodle.
Some material is also available from previous iteration of the seminar. Note however, that the current iteration will place less of an emphasis on dependent type theory.
Literature
The following papers and books give introductions to type theory. They are listed in no particular order.
- Avigad 2020, Foundations.
A fairly broad introduction to the foundations of modern proof assistants, including dependent type theory. Nice overview of the main concepts. - Pierce 2002, Types and Programming Languages. Popular textbook on different (non-dependent) type systems. Available in the university library.
- Barthe/Coquand 2000, An Introduction to Dependent Type Theory
- Angiuli and Gratzer 2024, Principles of Dependent Type Theory
- Girard/Lafont/Taylor 1989, Proofs and Types
- Mimram 2020, PROGRAM = PROOF
- Barendregt 1993, Lambda Calculi with Types
The standard introduction to the simply-typed lambda calculus and pure type systems. - Homotopy Type Theory Book, Ch. 1.
While this book is about homotopy type theory, the first chapter gives a nice introduction to standard dependent type theory. - Hoffmann 1997, Syntax and Semantics of Dependent Types
A fairly brief introduction to the category-theoretical semantics of type theories. Only relevant for topics involving category theory.
Topics
The following topics would be suitable for this seminar. More topics will be added in the following weeks.
If you'd like to work on a topic not listed here, please contact me. Some additional ideas for dependent type theory are available here. You can also take a look at the publications in the Workshop on Type-driven Development.
I provide at least one relevant paper about each topic, but it'll often be useful to look at other sources as well. To find these, look at the sources cited by your paper and look at other papers that cite your paper (using, e.g., Google Scholar's "Cited by" search). If you can't access a paper, look at the authors' webpages. They often link to a freely accessible PDF of the paper, or at least to a 'preprint' version which is substantially identical to the published version. If that fails, ask me and I'll get the paper for you.
Polymorphism is not set-theoretic
The simply-typed lambda calculus has a set-theoretic semantics that interprets types as sets, and terms as functions between them. This semantics can not be extended to a polymorphic extension of the lambda calculus.
Parametric Polymorphism
A basic example of a parametric polymorphism in Haskell is the type signature a -> a, which is so restrictive that there is only one (total) function of that type, namely the identity function. Loosely speaking parametrically polymorphic functions have to act ''uniformly'' on all types. This idea can be made precise using relational semantics.
Bidirectional Type Checking
Coquand, 1996Pierce, Turner 2000
Naive approaches to type-checking dependent types require the user to provide explicit type annotations in many places. Bidirectional type checkers are a popular class of type checking algorithms that perform a limited form of type inference, lessening the annotation-burdern on the user.
Indexed Inductive Types
Indexed inductive types (also known as inductive families) are a core feature of all mainstream dependent type theories. They can be used to define a very large class of useful types: (dependent) sums, (dependent) products, lists, trees, vectors, and so on. So by adding indexed inductive types to a type theory, we get a lot of constructions all at once.
Induction-Recursion
Inductive-recursive types are a generalisation of (indexed) inductive types. They allow a function f over a data type D to be defined simultaneously with D (so f and D may refer to each other). This seemingly trivial extension has far-reaching consequences: it increases the logical strength of a type theory ("how many statements can be proven in it?") considerably.
Induction-Induction
Forsberg/Setzer 2012
Kaposi/Kovács/Lafont
Similar to inductive-recursive types, inductive-inductive types allow us to define two inductive types D and E simultaneously. Surprisingly, this extension does not increase the logical strength of the theory at all if D and E are finitely branching.
Indexed Containers
Altenkirch/Ghani/Hancock/McBride/Morris 2015
Indexed containers are a type, definable in standard type theories, that captures all indexed inductive types. This means that every indexed inductive type is isomorphic to an indexed container (and vice versa).
Dependent Pattern Matching With K
Dependent pattern matching is a variant of regular pattern matching for indexed inductive types. This older paper presented the first method for implementing dependent pattern matching by translating it to applications of eliminators of inductive types. The translation uses axiom K, the principle of uniqueness of identity proofs.
Dependent Pattern Matching Without K
This newer paper shows how to implement dependent pattern matching without using axiom K. This makes it compatible with homotopy type theory.
Structural Termination Checking
Type theories which support recursive functions need to ensure that these functions always terminate. One way to do this is with a structural termination checker that accepts a large class of terminating functions.
Sized Types
Sized types are a type-based method for checking termination. They are conceptually attractive because, unlike structural termination checkers, they are compositional.
Homotopy Type Theory
Homotopy type theory extends type theory with the univalence axiom, which states, very informally, that isomorphic objects are equal. This gives us a much richer notion of equality between types than that available in standard type theories.
Cubical Type Theory
Cohen/Coquand/Huber/Mörtberg 2015
Cubical type theory is an implementation of homotopy type theory. It internalises the univalence axiom, so univalence is provable in the theory. This requires a fairly large set of new constructs.
Observational Type Theory
Altenkirch/McBride/Swierstra 2007
Observational type theory extends type theory with additional constructs that can be used to prove, in particular, function extensionality (i.e., two functions are equal if they map the same inputs to the same outputs). It can be seen as a halfway point between 'standard' type theory and homotopy type theory.
Self Types
Self types are a fascinating type-theoretic feature that allows us to encode inductive types, rather than taking them as primitive. They are implemented in the Cedille theorem prover, whose core type theory is, as a result, both very small and very powerful.
Rewrite Rules
Cockx/Tabareau/Winterhalter 2021
In a standard type theory, we can have either 0 + n = n or n + 0 = n as a definitional equation, but not both. Rewrite rules allow us to register additional definitional equations (at our own peril), enabling more proofs by computation.
Pure Type Systems and the Lambda Cube
Dependent type theories allow many forms of dependency between values and types. If we restrict these dependencies, we get weaker but still useful theories.
Type Theory in Type Theory
If we want to prove properties of our type theories, we should of course do so in a type-theoretic theorem prover. But this, it turns out, poses quite profound challenges.
Assembly in Type Theory
Kennedy/Benton/Jensen/Dagand 2013
If we want to prove properties about other programming languages, we should of course also do so in a type-theoretic theorem prover. This paper formalises a subset of x86 assembly, which makes for a nice contrast with the previous formalisation of a very high-level language.
Locally Cartesian Closed Categories
Locally cartesian-closed categories (LCCC) provide a category-theoretical semantics of type theory. This means, roughly, that we can interpret any term of a type theory as a morphism in a given LCCC. This correspondence implies a deep connection between category theory and type theory, to the point where many researchers consider the two fields essentially the same.
Categories With Families
Castellan/Clairambault/Dybjer 2021Hofmann 2009
Categories with families provide an alternative category-theoretical semantics for type theory.