A categorical quantum logic

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 ly normalising cut-elimination. This syntax encodes abstract qualitative and quantitative information about the behaviour of quantum processes.

• Type: Journal
• Year: 2006
• Where: MSCS
• Authors: Samson Abramsky, Ross Duncan
• Keywords: Abstract Qualitative, MSCS 2006, Proof-net Syntax, Sequent Calculus