A Categorical Quantum Logic
Samson Abramsky and Ross Duncan
We define a sequent calculus corresponding to the logic of strongly compact closed categories with biproducts. Based on this calculus, we define a proof-net syntax with a strongly normalising cut-elimination. This syntax encodes abstract qualitative and quantitative information about the behaviour of quantum processes.