ABSTRACT. It is possible to design proof systems for a vast range of logics, including all the common ones, by adopting two general proof constructors:

(1) the subatomic shape recently introduced by Andrea Aler Tubella, and

(2) a very general notion of formal substitution that is currently being explored by Benjamin Ralph and that subsumes standard quantification.

The two constructors could be considered two design principles, or, in other words, two ways of looking at proofs. In this talk, I will show how, by adopting them, we get a good starting point for designing proof systems that naturally yield canonical proofs of minimal size and that allow for a unified normalisation theory.