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.
infobook 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 |
links
BibTeX
Link (pdf)
related pages
|