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.

Creative Commons BY 4.0

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

Please log in to DOOR to see more details.

• Peter Arndt (Heinrich-Heine-Universität Düsseldorf, DE)
• Steve Awodey (Carnegie Mellon University - Pittsburgh, US) [dblp]
• Andrej Bauer (University of Ljubljana, SI) [dblp]
• Karim Johannes Becher (University of Antwerp, BE)
• Olaf Beyersdorff (Friedrich-Schiller-Universität Jena, DE) [dblp]
• Marc Bezem (University of Bergen, NO)
• Ingo Blechschmidt (Universität Augsburg, DE)
• Ulrik Buchholtz (University of Nottingham, GB) [dblp]
• Gabriele Buriola (University of Verona, IT)
• Felix Cherubini (Chalmers University of Technology - Göteborg, SE)
• Michel Coste (University of Rennes, FR) [dblp]
• Laura Crosilla (University of Florence, IT)
• Nicolas Daans (Charles University - Prague, CZ)
• Dominique Duval (University of Grenoble, FR)
• Martín H. Escardó (University of Birmingham, GB) [dblp]
• Giulio Fellin (University of Verona, IT)
• Makoto Fujiwara (Tokyo University of Science, JP) [dblp]
• Hugo Herbelin (Université Paris Cité, FR) [dblp]
• Matthias Hutzler (University of Gothenburg, SE)
• Hajime Ishihara (Toho University - Chiba, JP) [dblp]
• Ulrich Kohlenbach (TU Darmstadt, DE) [dblp]
• Henri Lombardi (University of Franche-Comté - Besancon, FR) [dblp]
• Maria Emilia Maietti (University of Padova, IT) [dblp]
• Julien Narboux (University of Strasbourg, FR) [dblp]
• Sara Negri (University of Genova, IT) [dblp]
• Takako Nemoto (Tohoku University - Sendai, JP) [dblp]
• Stefan Neuwirth (University of Franche-Comté - Besancon, FR)
• Satoru Niki (Ruhr-Universität Bochum, DE)
• Paige North (Utrecht University, NL)
• Eugenio Orlandelli (University of Bologna, IT) [dblp]
• Edi Pavlovic (LMU München, DE) [dblp]
• Iosif Petrakis (University of Verona, IT)
• Elaine Pimentel (University College London, GB) [dblp]
• Michael Rathjen (University of Leeds, GB) [dblp]
• Marie-Françoise Roy (Université de Rennes 1 - Rennes Cedex, FR) [dblp]
• Peter M. Schuster (University of Verona, IT) [dblp]
• Monika Seisenberger (Swansea University, GB) [dblp]
• Sana Stojanovic-Djurdjevic (University of Belgrade, RS) [dblp]
• Benno van den Berg (University of Amsterdam, NL)
• Steven J. Vickers (University of Birmingham, GB) [dblp]