Noncommutative logic
Noncommutative logic is an extension of linear logic that combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek calculus. Its sequent calculus relies on the structure of order varieties (a family of cyclic orders that may be viewed as a species of structure), and the correctness criterion for its proof nets is given in terms of partial permutations.