This paper displays a linear sequent calculus in accordance with the no-cloning and no-deleting theorems of quantum computing. The calculus represents typing operations on matrices in terms of linear sequent rules, satisfing admissibility of cut. It is possible to define a strict monoidal categorical semantics for it using categories generated by finite vector spaces extended with a Kronecker product, which can be viewed as the dual of an approach proposed by Abramsky-Coecke.