TOP
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
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
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)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/24021

Organizers

Contact

Dagstuhl Reports

As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.

  • Upload (Use personal credentials as created in DOOR to log in)

Dagstuhl Seminar Wiki

Shared Documents

Schedule

Motivation

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

Participants

Related Seminars
  • Dagstuhl Seminar 21472: Geometric Logic, Constructivisation, and Automated Theorem Proving (2021-11-21 - 2021-11-26) (Details)

Classification
  • Logic in Computer Science

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