Substructural logics are logical systems lacking one or more structural rules among exchange, weakening and contraction. Notable instances of substructural logics include Girard's linear logic and its non-commutative variants, among which prominently figures the syntactic calculus of Lambek. Motivated by application in linguistics, proof-theorists have also studied logics lacking more primitive structural rules, such as associativity.

In this talk, I will introduce semi-associative substructural logics, which are logical systems allowing only a restricted, directed version of associativity. The motivation for studying these logics come from their categorical models, which are Street's skew monoidal closed categories. I will present a cut-free sequent calculus, presenting the free skew monoidal closed category on a set of atomic formulae. Then I will discuss some proof-theoretic results: proof normalization, extensions with additive connectives and, time permitting, Craig interpolation.