Theory and Application of Formal Proofs

November 5–7, 2013

in association with the international workshop on
Proof Search in Axiomatic Theories and Type Theories

Collected Abstracts

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

Proof Checking

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

Proof Search

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