Dagstuhl Seminar 26121
Proof Systems in Actual Practice: Reasoning and Computation
( Mar 15 – Mar 20, 2026 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/26121
Organizers
- Ingo Blechschmidt (University of Antwerp, BE)
- Liron Cohen (Ben Gurion University - Be'er Sheva, IL)
- Thierry Coquand (University of Gothenburg, SE)
- Peter M. Schuster (University of Verona, IT)
Contact
- Marsha Kleinbauer (for scientific matters)
- Christina Schwarz (for administrative matters)
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
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
A great success of 20th-century mathematical logic has been the development of proof systems for putting mathematics on a firm basis, clarifying foundational options and their interaction. However, a pivotal question arises: Can these proof systems extend beyond foundational theory to offer practical benefits in mathematics and computer science? In particular, do proof systems facilitate proofs of new results, better or automated proofs of established results, or computer formalization of specific subjects in mathematics and computer science?
A partial positive answer is given by synthetic frameworks for specific subjects in mathematics and computer science, the most well-known of which presumably is Euclid's synthetic geometry. Unlike Descartes' coordinate-centered analytic geometry, where points and lines are encoded as (pairs or sets of) numbers, the synthetic account puts points and lines as primitive concepts governed only by axioms. As such, synthetic geometry provides custom-tailored foundations to geometry. Synthetic frameworks have proved to be pivotal tools at the interface of mathematics and computer science, especially in enabling concise formalizations. Way beyond Euclid's synthetic geometry, noteworthy present achievements include homotopy type theory, synthetic computability theory, synthetic differential geometry and synthetic algebraic geometry.
Further affirmative answers emerge from logic-driven computational algebra and geometry, and the proof assistants centered on coherent logic. These topics are interconnected through shared logical methodologies such as sheaf models, syntactic translations, novel developments in realizability theory, and strong negation for constructive reasoning with negative information. In particular, enhancing the current logical models of computation to incorporate computational side-effects from programming languages brings in new models with interesting properties.
This Dagstuhl Seminar seeks to extend and deepen the convergence across disciplinary boundaries by fostering exchange and collaboration among the relevant experts and practitioners, uniting expertise in proof theory with proof complexity, categorical semantics, constructive mathematics, proof mining, program extraction, and automated theorem proving. By bridging these domains, we seek to empower the next generation of researchers to frame and connect their work within this converging landscape, ultimately advancing the computational applications of proof systems in both theoretical and practical contexts.
Creative Commons BY 4.0
Ingo Blechschmidt, Liron Cohen, Thierry Coquand, and Peter M. Schuster
Please log in to DOOR to see more details.
- Peter Arndt (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
- Steve Awodey (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Andrej Bauer (University of Ljubljana, SI) [dblp]
- Ulrich Berger (Swansea University, GB) [dblp]
- Marc Bezem (University of Bergen, NO) [dblp]
- Ingo Blechschmidt (University of Antwerp, BE)
- Riccardo Borsetto (University of Verona, IT)
- Ulrik Buchholtz (University of Nottingham, GB) [dblp]
- Felix Cherubini (Universität Augsburg, DE)
- Liron Cohen (Ben Gurion University - Be'er Sheva, IL) [dblp]
- Thierry Coquand (University of Gothenburg, SE) [dblp]
- Tom de Jong (University of Nottingham, GB) [dblp]
- Martín H. Escardó (University of Birmingham, GB) [dblp]
- Yannick Forster (INRIA - Paris, FR) [dblp]
- Tobias Fritz (Universität Innsbruck, AT) [dblp]
- Hugo Herbelin (Paris Cité University, FR) [dblp]
- Maja Kadziolka (University of Warsaw, PL)
- Dominik Kirst (INRIA / IRIF - Paris) [dblp]
- Ryota Kuroki (University of Tokyo, JP)
- Henri Lombardi (Marie and Louis Pasteur University - Besançon, FR) [dblp]
- Assia Mahboubi (INRIA - Nantes, FR) [dblp]
- Alexandre Miquel (University of the Republic - Montevideo, UY)
- Sara Negri (University of Genova, IT) [dblp]
- Takako Nemoto (Tohoku University - Sendai, JP) [dblp]
- Stefan Neuwirth (Marie and Louis Pasteur University - Besançon, FR) [dblp]
- Marc Nieper-Wißkirchen (Universität Augsburg, DE) [dblp]
- Satoru Niki (Kanagawa University, JP) [dblp]
- Iosif Petrakis (University of Verona, IT) [dblp]
- Sebastian Posur (Universität Münster, DE) [dblp]
- Vincent Rahli (University of Birmingham, GB) [dblp]
- Michael Rathjen (University of Leeds, GB) [dblp]
- Reuben Rowe (Royal Holloway, University of London, GB) [dblp]
- Peter M. Schuster (University of Verona, IT) [dblp]
- Sana Stojanovic-Djurdjevic (University of Belgrade, RS) [dblp]
- Luna Strah (University of Ljubljana, SI)
- Benno van den Berg (University of Amsterdam, NL) [dblp]
- Steven J. Vickers (University of Birmingham, GB) [dblp]
- David Wärn (University of Gothenburg, SE) [dblp]
- Chuangjie Xu (SonarSource - Bochum, DE) [dblp]
Related Seminars
Classification
- Logic in Computer Science
Keywords
- logic-driven computational algebra and geometry
- sheaf models and new frontiers in realizability theory
- strong negation for constructive reasoning with negative information
- synthetic methods in computer science and mathematics
