Deep inference is a methodology for the design of proof formalisms, motivated by the pursuit of linearity in the composition mechanisms. Proofs can be composed not only by inference rules but also sequentially and horizontally by connective. This allows for proof systems in which all structural rules are decomposed to their atomic forms, supplemented by linear rule schemes which only move information around.

Subatomic logic is a recent area of development in deep inference in which even the atomic rules are given linearly, by taking atoms not as base elements of a proof but as non-commutative binary connectives whose arguments are their truth values.

I will present some recent work in a subatomic system for propositional classical logic, in particular the 'eversion lemma' and two of its applications, one of which has to do with proof compression and the other with cut elimination, and I will discuss some future directions for research.

Link to CSL paper