Proof Nets
A graph-theoretic syntax for proofs in Linear Logic introduced by Girard (1987). Where sequent calculus represents inessentially-distinct proofs as different proof trees (differing only in the order of independent rule applications), proof nets quotient that bureaucracy away — “morally the same” proofs become literally the same net. Cut elimination becomes graph rewriting and is strongly normalising. Proof nets are the linear-logic analogue of natural deduction; the corresponding dynamics is the formal counterpart of communication in concurrent Curry–Howard correspondences for Session Types.