Normalisation and Deep Inference

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.