A Categorical Quantum Logic
Samson Abramsky and Ross Duncan
Abstract
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.
Book Title
Proceedings of the 2nd International Workshop on Quantum Programming Languages
Edition
Selinger‚ Peter
Keywords
quantum computing; compact closed categories; proof−nets
Note
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.
Series
Turku Centre for Computer Science General Publication
Volume
33
Year
2004