Barcelona, August 3rd-14th 2015

Compact representation (left) of an equivalence class of proofs (right)

Advanced course - Week 1 - Paola Bruscoli

This course provides an introduction to the techniques and methods proper of deep inference, a recent methodology in proof theory that has been developed for the past 15 years. Purpose of the course is to provide participants with a detailed and compact presentation of the many features that deep-inference based proof systems exhibit. Through small examples and exercises mixed with usual presentations our aim is that of developing an initial technical understanding of deep inference, while simultaneously highlighting, through examples, the different scope of applicability of more traditional methods.

Introductory course - Week 2 - Anupam Das and Alessio Guglielmi

This course is mainly about understanding normalisation in proof theory by uncovering its local and geometric nature. We will use the tools of deep inference, which we could succinctly describe as an extreme form of linear logic. By doing so, we obtain a *better* proof theory than the traditional one due to Gentzen: we can provide proof systems for more logics, with smaller proofs, less syntax, less bureaucracy and we have a chance to make substantial progress towards a solution to the century-old problem of the *identity of proofs*.

Slides: handout, strip-tease

20.8.2015 Alessio Guglielmi email