19. – 24. August 2018, Dagstuhl-Seminar 18341

Formalization of Mathematics in Type Theory


Andrej Bauer (University of Ljubljana, SI)
Martín H. Escardó (University of Birmingham, GB)
Peter L. Lumsdaine (University of Stockholm, SE)
Assia Mahboubi (INRIA – Nantes, FR)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 8, Issue 8 Dagstuhl Report


We and all the participants were delighted to benefit from Dagstuhl's inspiring environment.

Proof assistants are receiving increased attention from users with a background in mathematics, as opposed to their traditional users from theoretical computer science/logic/program verification, and this was the major focus of the meeting. This is true in particular of proof assistants based on dependent types, probably due in part to the advent of homotopy type theory, developed in the proof assistants Coq, Agda and Lean.

The audience of the seminar was thus rather unusual in composition, and featured several experienced researchers used to attending seminars at the Mathematisches Forschungsinstitut Oberwolfach, and visiting Schloss Dagstuhl for the first time. In order to foster discussion and fuse collaborations, we adopted a different format from the standard string of slide-based talks: talks in the morning, so that people get to know the work of each other, and working in groups in the afternoon. At the end of each day, before dinner, each group presented a summary of the outcomes of their meetings to all participants, which allowed inter-group discussion and collaboration. This had been tried before by some of the organizers, in the course of Dagstuhl seminar 16112, and worked just as well in our case.

Working group topics were proposed by the audience on the first day, by giving short presentations of a few minutes and writing topics in the board. Some were quite specialized and homogeneous (e.g. the cubical type theory group), and allowed people to have a focussed collaborative brainstorming on a specific open problem of the field. Some were more open-ended, and allowed people to confront various approaches to the same issue/concept in different systems (different proof assistants, computer algebra systems, etc.).

Some people did applied work, such as trying to compute the so-called Brunerie number from an existing proof in homotopy type theory, in order to identity and fix inefficiency problems in proofs assistants based on cubical type theory. Some people used their spare time to solve the ``Dagstuhl dinner'' problem. Details of the topics discussed are in the reports produced by each group.

This was a rather productive meeting, and people from different scientific backgrounds not only met but talked together effectively, solving and identifying problems to work on collaboratively in future.

Summary text license
  Creative Commons BY 3.0 Unported license
  Andrej Bauer, Martín H. Escardó, Peter L. Lumsdaine, and Assia Mahboubi


  • Semantics / Formal Methods
  • Verification / Logic


  • Formalized mathematics
  • Type theory
  • Proof assistant
  • Formal methods


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.