You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Mar 23 2023 at 21:19):This has been out for a month and half, but I was just catching up to stuff on here, so figured I would post: The Quantum Effect: A Recipe for QuantumPi with abstract:
Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus answer positively the question whether a computational effect exists that turns reversible classical computation into quantum computation: the quantum effect. Measurements can be added by layering a further effect on top. Our construction also enables some reasoning about quantum programs (with or without measurement) through a combination of classical reasoning and reasoning about complementarity.
with @Chris Heunen @Robin Kaarsgaard and Amr Sabry. Quite a lot of the paper is implemented in Agda - it is possible to run small QuantumPi programs as well as do reasoning on them.
Rig categories seems to be popular right now, so here's one more item that uses them, along with a bunch of other categorical constructions.