in association with the international workshop on

Proof Search in Axiomatic Theories and Type Theories

Formal proofs are becoming increasingly important in a number of domains in computer science and mathematics. The topic of the colloquium is structural proof theory, broadly construed. Some examples of relevant topics:

Sequential and parallel structure in proofs; sharing and duplication of proofs; permutation of proof steps; canonical forms; focusing; polarities; graphical proof syntax; proof complexity; cut-eliminiation strategies; CERes

Generating, transmitting, translating, and checking
proof objects; universal proof languages; proof
certificates; proof compression; cut-introduction;
certification of high-performance systems (SMT,
resolution, *etc.*)

Automated and interactive proof search in constrained
logics (linear, temporal, bunched,
probabilistic, *etc.*); mixing deduction and
computation; induction and co-induction; cyclic proofs;
computational interpretations