Links und Funktionen


Inhaltsbereich

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 3 sessions at the start of the term in which I introduce the key concepts and notations of type theory. These sessions 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 dates and topics.

Date Topic
17.04. lecture DTT 1
24.04. lecture DTT 2
30.04. (Tuesday) lecture DTT 3
08.05. lecture Writing
TBA student presentations
TBA student presentations
TBA student paper submissions

Literature

The following papers and books give introductions to type theory. They are listed in no particular order.

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

Dybjer 1994

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

Dybjer 2000

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

Goguen/McBride/McKinna 2006

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

Cockx/Devriese/Piessens 2014

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

Abel 1998

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

Abel/Pienkta 2016

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

HoTT book, Ch. 1-3

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

Stump 2018

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

Barendregt 1991

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

Abel/Öhman/Vezzosi 2017

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

Seely 1984
Hofmann 2005

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


Funktionsleiste