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

Dagstuhl Seminar 24341

Proof Representations: From Theory to Applications

( Aug 18 – Aug 23, 2024 )

Please use the following short url to reference this page:



Dagstuhl Seminar Wiki

Shared Documents

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


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.

Copyright Carlos Areces, Anupam Das, Elaine Pimentel, and Lutz Straßburger


  • Artificial Intelligence
  • Logic in Computer Science
  • Programming Languages

  • proof theory
  • proof calculi
  • computational interpretations
  • proof semantics
  • dynamic operators