Summary: we expose a syntax for non-commutative intuitionistic logic in a "linear" fashion and we define the corresponding proof-theory with slices. We achieve:
(1) implicit box-building and sequentialisation in the general case
(2) strong confluence by cut-reductions for any single slice
(3) strong normalization for the implicational-free fragment