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