Deep inference is a new proof theoretic methodology that conserves the results of traditional formalisms, like the sequent calculus, but doesn't suffer from many of their shortcomings. The basic idea is to get rid of the meta (or structural) level in deductive systems, because this is too biased by classical logic.

In deep inference, there's enormous freedom in designing inference rules, and this, of course, is dangerous: we could create monsters. So, much of the research in deep inference has been about bringing method into chaos. We broadly developed the proof theory of a formalism, called the `calculus of structures', which is the most basic expression of deep inference.

The calculus of structures allows for the systematic and modular expression of analytic deductive systems for the vastest array of logics. For classical logic, it provides exponential speed-ups over the proof complexity of analytic sequent calculus. There are logics, closely connected to process algebras like CCS, which only can be expressed with deep inference, and they are expressed in the calculus of structures. Deductive systems in the calculus of structures enjoy several normalisation and locality properties that cannot be obtained without deep inference.

Designing syntax is, of course, a very semantic activity. One future research direction of deep inference is to attack the problem of bureaucracy in proofs, i.e., the mismatch between syntax and semantics. This will hopefully yield good answers to the question: `When are two given proofs the same?'.

You can find a more thorough introduction (and papers, etc.) on the page: http://alessio.guglielmi.name/res/cos.