An introduction to deep inference

Andrea Aler Tubella (IRIF, CNRS & Univ. Paris Diderot, France) and Lutz Stra├čburger (INRIA Saclay, Ile-de-France)

In deep inference formalisms, inference rules can be applied at any depth inside the proof. In this introductory course, we will provide a clear understanding of the intuitions behind deep inference, together with a rigorous account of the properties that deep inference proof systems enjoy, especially in regards to normalisation. Deep inference proof systems enjoy properties that particularly stand out: atomicity, locality and regularity. Normalisation procedures specific to deep inference allow for new notions of normal forms for proofs, as well as for a general modular cut-elimination theory. Furthermore, the ability to track every occurrence of an atom throughout a proof allows for the definition of geometric invariants with which it is possible to normalise proofs without looking at their logical connectives or logical rules, obtaining a purely geometric normalisation procedure. Beyond normalisation, in deep inference it is possible to type optimised versions of the lambda-calculus.