The calculus of structures is a proof theoretical formalism, like natural
deduction and the sequent calculus, for specifying logical systems and studying
their properties. In this talk I will present its basic principles and its main
features. For example, due to a new up-down symmetry, the identity axiom and
the cut rule become syntactically dual. This allows to reduce the cut to an
atomic version without going through a cut elimination argument. Furthermore,
in the calculus of structures one can present new types of inference rules that
allow to design logical systems that are completely local. More precisely, the
contraction rule can be reduced to an atomic version (in the same way as it is
usually done for the identity), and the promotion rule of linear logic can be
presented in a local form. I will also present decomposition theorems which
provide new types of normal forms for proofs and which are independent from cut
elimination.