  Thirty years ago, I introduced a non-commutative variant of classical linear
logic, called "pomset logic", issued from a particular categorical
interpretation of linear logic known as coherence spaces. In addition to the
usual commutative multiplicative connectives of linear logic, pomset logic
includes a non-commutative connective, "$\triangleleft$" called "before",
associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft
B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered
MultiSET of formulas. Pomset logic enjoys a proof net calculus with
cut-elimination, denotational semantics, and faithfully embeds sequent
calculus.
  The study of pomset logic has reopened with recent results on handsome proof
nets, on its sequent calculus, or on its following calculi like deep inference
by Guglielmi and Strassburger. Therefore, it is high time we published a
thorough presentation of pomset logic, including published and unpublished
material, old and new results.
  Pomset logic (1993) is a non-commutative variant of linear logic (1987) as
for Lambek calculus (1958!) and it can also be used as a grammatical formalism.
Those two calculi are quite different, but we hope that the algebraic
presentation we give here, with formulas as algebraic terms and with a semantic
notion of proof (net) correctness, better matches Lambek's view of what a logic
should be.
