Master Seminar: Dependent Type Theory
Instructor: Jannis Limperg
Content
Dependent type theories (or just type theories) are formal systems which can be understood both as powerful logics and functional programming languages. They have been studied since the late 1960’s and today serve as the foundations of popular interactive theorem provers such as Agda, Coq, Idris and Lean. In this seminar, we will discuss various important type theories 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 in which I introduce the key concepts and notations of type theory. These lectures should give you the background knowledge required to understand type theory papers. I’ll additionally give one lecture on academic writing.
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 type theory, type-theoretic construction or proof method. I provide some suitable topics below, 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. We won’t have additional meetings before the talks, but you can always ask questions on the course chat (see below).
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.
The report must be in German or English. The talk must be in English.
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:
Server: https://chat.ifi.lmu.de
Stream: TCS-24S-DTT
I’ll post organisational announcements only to this stream, so do join. Please ask questions there so that everyone can read the answers.
Schedule
We meet periodically on Wednesdays (with exceptions) from 12:15 to 13:45 (both s.t.) at Oettingenstraße 67, room L109. See below for the exact schedule.
| Date | Topic | Room |
|---|---|---|
| Wed 17.04. | lecture DTT 1 | Oettingenstr. 67 L109 |
| Wed 24.04. | lecture DTT 2 | Oettingenstr. 67 L109 |
| Tue 30.04. | lecture DTT 3 | Oettingenstr. 67 L109 |
| Wed 08.05. | lecture DTT 4 | Oettingenstr. 67 L109 |
| Wed 15.05. | lecture DTT 5 | Oettingenstr. 67 L109 |
| Wed 22.05. | lecture Writing | Oettingenstr. 67 L109 |
| Mon 01.07. 12:15 - 17:45 | student presentations | Theresienstr. 39B 046A |
| Tue 02.07. 10:15 - 13:45 | student presentations | Theresienstr. 39B 133A |
| Fri 06.09. | student paper submissions |
Literature
There are work-in-progress lecture notes for this seminar. I will update them periodically.
Slides for the writing lecture are also available.
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 type theory. Nice overview of the main concepts. - 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 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. If you’d like to work on a topic not listed here, please contact me. Some additional ideas are available here.
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.
Indexed Inductive Types
Indexed inductive types (also known as inductive families) are a core feature of all mainstream 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 2021
Categories with families provide an alternative category-theoretical semantics for type theory.
Artikelaktionen