May 10 – 15 , 2020, Dagstuhl Seminar 20202

RESCHEDULED Geometric Logic, Constructivisation, and Automated Theorem Proving

Due to the Covid-19 pandemic, this seminar was rescheduled to November 21 – 26 , 2021Seminar 21472.


Thierry Coquand (University of Gothenburg, SE)
Hajime Ishihara (JAIST – Ishikawa, JP)
Sara Negri (University of Genova, IT)
Peter M. Schuster (University of Verona, IT)

For support, please contact

Dagstuhl Service Team


Right at the origin of the development of the modern concepts of proof and computation, fundamental both to mathematics and computer science, Brouwer was advocating the exclusive use of effective methods of proof, designed intuitionism, whereas Hilbert was arguing that non-effective methods are important for the progress of mathematics, viewing constructivisation as an activity to take place after the fact. While the Brouwer–Hilbert debate arose from epistemological concerns about mathematics, the interplay between effective and non-effective proof has become more and more relevant since the advent of theoretical and actual computing devices: We now know that, to a certain extent, intuitionistic logic can be seen as the logic of computation.

A central question has remained from that discussion: What is the extent of intuitionistic mathematics? Ordinal analysis is an attempt to describe how strong subsystems of analysis can be proved consistent in intuitionistic mathematics. Another foundational solution, with the goal of rebuilding mathematics constructively, is aimed at by Bishop-style constructive mathematics and by Martin-Löf’s intuitionistic type theory, the latter most recently in the form of the so-called homotopy or univalent type theory put forward by Voevodsky.

From a more practical angle, the question rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is done by manipulating proofs mechanically and/or by adequate metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof analysis, proof mining, etc.). In this vein, the central question should be put as follows: What is the computational content of proofs?

This Dagstuhl Seminar will be guided by this central question, putting a special focus on coherent and geometric theories and their generalisations: for they are (a) fairly widespread in mathematics and non-classical logics such as temporal and modal logics, (b) a priori amenable for constructivisation (Barr’s Theorem), and (c) particularly suited as a basis for automated theorem proving. Specific topics include (i) categorical semantics for geometric theories, (ii) complexity issues of and algorithms for geometrisation of theories including speed-up questions, (iii) the use of geometric theories in constructive mathematics including finding algorithms, (iv) proof-theoretic presentation of sheaf models and higher toposes and (v) coherent logic for obtaining automatically readable proofs.

Seminar presentations of recent research and refresher tutorials of ground knowledge will be complemented by parallel work groups on the relevant topics. Tutorials of two hours each are planned about proof theory of geometric logic, sheaf models and constructive algebra, proof mining and program extraction in axiomatic environments, and automated theorem proving with coherent logic.

Motivation text license
  Creative Commons BY 3.0 DE
  Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Dagstuhl Seminar Series


  • Data Structures / Algorithms / Complexity
  • Semantics / Formal Methods
  • Verification / Logic


  • Geometric logic
  • Constructivisation
  • Automated theorem proving
  • Proof theory
  • Categorical semantics


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.