16. – 21. Oktober 2016, Dagstuhl-Seminar 16421

Universality of Proofs


Gilles Dowek (INRIA & ENS Cachan, FR)
Catherine Dubois (ENSIIE – Evry, FR)
Brigitte Pientka (McGill University – Montreal, CA)
Florian Rabe (Jacobs University Bremen, DE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 6, Issue 10 Dagstuhl Report
Programm des Dagstuhl-Seminars [pdf]


Proof systems are software systems that allow us to build formal proofs, either interactively or automatically, and to check the correctness of such proofs. Building such a formal proof is always a difficult task -- for instance the Feit-Thompson odd order theorem, the CompCert verified C compiler, the seL4 verified operating system micro-kernel, and the proof of the Kepler conjecture required several years with a medium to large team of developers to be completed. Moreover, the fact that each of these proofs is formalized in a specific logic and the language of a specific proof tool is a severe limitation to its dissemination within the community of mathematicians and computer scientists. Compared to many other branches of computer science, for instance software engineering, we are still very far from having off-the-shelf and ready-to-use components, "proving in the large" techniques, and interoperability of theory and systems. However, several teams around the world are working on this issue and partial solutions have been proposed including point-to-point translations, proof standards, and logical frameworks. Yet, a lot still remains to be done as there is currently no overarching general foundation and methodology.

This seminar has been organized to bring together researchers from different communities, such as automated proving, interactive proving and SAT/SMT solving as well as from logic, proof engineering, program verification and formal mathematics. An essential goal has been to form a community around these issues in order to learn about and reconcile these different approaches. This will allow us to develop a common objective and framework for proof developments that support the communication, reuse, and interoperability of proofs.

The program of the seminar included introductions to different methods and techniques, the definition of precise objectives, and the description of recent achievements and current trends. It consisted of 30 contributed talks from experts on the above topics and six breakout sessions on major problems: theory graph -- based reasoning, benchmarks, conflicting logics and system designs, proof certificates, design of a universal library of elementary mathematics, and a standard for system integration and proof interchange. The contributed talks took place in the morning, and two parallel breakout sessions each took place on Monday, Tuesday and Thursday afternoon, followed by plenary discussions organized by each session's moderator.

The organizers would like to thank the Dagstuhl team and all the participants for making this first seminar a success and, hopefully, an event to be repeated.

Summary text license
  Creative Commons BY 3.0 Unported license
  Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe


  • Semantics / Formal Methods
  • Verification / Logic


  • Logics
  • Formal proofs
  • Provers
  • Reusability
  • Interoperability
  • Logical frameworks
  • Proof formats
  • Translation


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.