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.
Proceedings of the 2nd International Workshop on Quantum Programming Languages
quantum computing; compact closed categories; proof−nets
This paper is largely superceded by the MSCS publication with the same title‚ however some details‚ such as the sequent calculus presentation‚ are only found in this version.
Turku Centre for Computer Science General Publication