Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 24021

From Proofs to Computation in Geometric Logic and Generalizations

( Jan 07 – Jan 12, 2024 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



Shared Documents



What is the computational content of proofs? This is one of the main topics in mathematical logic, especially proof theory, that is of relevance for computer science. The well-known foundational solutions aim at rebuilding mathematics constructively almost from scratch, and include Bishop-style constructive mathematics and 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 perhaps more practical angle, however, 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 mining, etc.).

A crucial role for answering these questions is played by coherent and geometric theories and their generalizations: not only that they are fairly widespread in modern mathematics and non-classical logics (e.g., in abstract algebra, and in temporal and modal logics); those theories are also a priori amenable for constructivisation (see Barr’s Theorem, especially its proof-theoretic variants, and the numerous Glivenko–style theorems); last but not least, effective theorem-proving for coherent theories can be automated with relative ease and clarity in relation to resolution.

Specific topics that substantially involve computer science research include categorical semantics for geometric theories up to the proof-theoretic presentation of sheaf models and higher toposes; extracting the computational content of proofs and dynamical methods in quadratic form theory; the interpretation of transfinite proof methods as latent computations; complexity issues of and algorithms for geometrization of theories; the use of geometric theories in constructive mathematics including finding algorithms, ideally with integrated developments; and coherent logic for obtaining automatically readable proofs.

To address those and related issues, this Dagstuhl Seminar will require deep interaction between experienced senior scientists and outstanding young researchers (PhD students and postdocs), uniting expertise in proof theory with proof complexity, categorical semantics, constructive mathematics, proof mining, program extraction and automated theorem proving. Seminar presentations of recent research and refresher tutorials of ground knowledge, including practical introductions to proof assistants, will be complemented by parallel working groups on up-to-date topics.

Copyright Ingo Blechschmidt, Thierry Coquand, Hajime Ishihara, and Peter M. Schuster


Related Seminars
  • Dagstuhl Seminar 21472: Geometric Logic, Constructivisation, and Automated Theorem Proving (2021-11-21 - 2021-11-26) (Details)
  • Dagstuhl Seminar 26121: Proof Systems in Actual Practice: Reasoning and Computation (2026-03-15 - 2026-03-20) (Details)

  • Logic in Computer Science

  • geometric logic
  • constructivisation
  • automated theorem proving
  • proof theory
  • categorical semantics