Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Innerhalb dieser Seite:
Externe Seiten:
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp

Dagstuhl-Seminar 24021

From Proofs to Computation in Geometric Logic and Generalizations

( 07. Jan – 12. Jan, 2024 )

(zum Vergrößern in der Bildmitte klicken)

Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:



Gemeinsame Dokumente



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


Verwandte Seminare
  • 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