Dagstuhl Seminar 24341
Proof Representations: From Theory to Applications
( Aug 18 – Aug 23, 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/24341
Organizers
- Carlos Areces (National University - Córdoba, AR)
- Anupam Das (University of Birmingham, GB)
- Elaine Pimentel (University College London, GB)
- Lutz Straßburger (INRIA Saclay - Île-de-France, FR)
Contact
- Marsha Kleinbauer (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Proof theory is the study of formal proofs as mathematical objects in their own right. The subject has enjoyed continued attention among computer scientists in particular due to its significance for formalization, metalogic, and automation. In recent decades there has been a surge of interest on the representations of formal proofs themselves. The outcomes of these investigations have been remarkable, in particular extending the scope of structural proof theory to novel and richer settings:
- Richer line structures (e.g. hypersequents, nested sequents, labelled sequents) have resulted in a uniform treatment of standard modal logics, streamlining their metatheory and providing new tools for metalogical problems.
- Richer proof structures (e.g., cyclic proofs, annotated systems, infinitely branching proofs) have significantly advanced our understanding of fixed points and (co)induction. Indeed, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic.
- Graphical proof representations (e.g., proof nets, atomic flows, combinatorial proofs) originating from “linear” logics, now not only comprise a well-behaved computational model for resource-sensitive reasoning, but also provide an impressively uniform treatment for logics across the board.
In fact, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic, which has produced deep and fruitful cross-fertilizations between programming languages and proof theory. Arguably, the most well-known is the Curry-Howard correspondence (“propositions-as-types”) where (functional) programs correspond to formal proofs and their execution to normalization. A complementary tradition, proof-search-as-computation (“propositions-as-processes”), instead interprets (logic) programs to formulas and their execution to proof search.
The point of this Dagstuhl Seminar is twofold. First and foremost, we want to bring together theorists and practitioners exploiting proof representations to identify new directions of application and, simultaneously, distill new theoretical directions from problems “in the wild”. At the same time, this seminar will expose the interface between the proof-normalization and proof-search traditions by probing proof representations from both directions.
Creative Commons BY 4.0
Carlos Areces, Anupam Das, Elaine Pimentel, and Lutz Straßburger
Please log in to DOOR to see more details.
- Matteo Acclavio (University of Southern Denmark - Odense, DK) [dblp]
- Bahareh Afshari (University of Gothenburg, SE) [dblp]
- Sara Ayhan (Ruhr-Universität Bochum, DE) [dblp]
- Eben Blaisdell (University of Pennsylvania - Philadelphia, US) [dblp]
- Yll Buzoku (University College London, GB) [dblp]
- Kaustuv Chaudhuri (INRIA Saclay - Île-de-France, FR) [dblp]
- Zhibo Chen (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Anupam Das (University of Birmingham, GB) [dblp]
- Abishek De (University of Birmingham, GB)
- Amy Felty (University of Ottawa, CA) [dblp]
- Alexander Gheorghiu (University College London, GB) [dblp]
- Marianna Girlando (University of Amsterdam, NL) [dblp]
- Rajeev P. Gore (Turner, AU) [dblp]
- Tao Gu (University College London, GB)
- Andrzej Indrzejczak (University of Lodz, PL) [dblp]
- Raheleh Jalali (The Czech Academy of Sciences - Prague, CZ) [dblp]
- Timo Lang (University College London, GB) [dblp]
- Anela Lolic (TU Wien, AT) [dblp]
- Bruno Lopes (Fluminense Federal University - Rio de Janeiro, BR) [dblp]
- Robin Martinot (Utrecht University, NL) [dblp]
- Dale Miller (INRIA Saclay - Île-de-France, FR) [dblp]
- Victor Nascimento (Universidade do Estado do Rio de Janeiro, BR)
- Sara Negri (University of Genova, IT) [dblp]
- Carlos Olarte (Université Sorbonne Paris Nord - Villetaneuse, FR) [dblp]
- Edi Pavlovic (LMU München, DE) [dblp]
- Elaine Pimentel (University College London, GB) [dblp]
- Ian Pratt-Hartmann (University of Manchester, GB) [dblp]
- Revantha Ramanayake (University of Groningen, NL) [dblp]
- Alexis Saurin (CNRS - Paris, FR) [dblp]
- Peter M. Schuster (University of Verona, IT) [dblp]
- Sana Stojanovic-Djurdjevic (University of Belgrade, RS) [dblp]
- Lutz Straßburger (INRIA Saclay - Île-de-France, FR) [dblp]
- Iris van der Giessen (University of Birmingham, GB) [dblp]
- Fernando Velázquez Quesada (University of Bergen, NO) [dblp]
- Heinrich Wansing (Ruhr-Universität Bochum, DE) [dblp]
- Richard Zach (University of Calgary, CA) [dblp]
Classification
- Artificial Intelligence
- Logic in Computer Science
- Programming Languages
Keywords
- proof theory
- proof calculi
- computational interpretations
- proof semantics
- dynamic operators
