# The ZX Seminar

Initiated at University of Oxford, the weekly ZX seminar provides a virtual venue for researchers to share their work related to the ZX calculus.

It is chaired by John van de Wetering, co-organized by Alexander Koziell-Pipe and Sarah Meng Li.

## Winter 2024 Schedule

**Wednesday January 10th: Optimizing ZX-Diagrams with Deep Reinforcement Learning**

**Speaker:**Maximilian Nägele (Max Planck Institute for the Science of Light)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Germany/Netherlands

**Abstract:**ZX-diagrams are a powerful graphical language for the description of quantum processes with applications in fundamental quantum mechanics, quantum circuit optimization, tensor network simulation, and many more. The utility of ZX-diagrams relies on a set of local transformation rules that can be applied to them without changing the underlying quantum process they describe. These rules can be exploited to optimize the structure of ZX diagrams for a range of applications. However, finding an optimal sequence of transformation rules is generally an open problem. In this work, we bring together ZX-diagrams with reinforcement learning, a machine learning technique designed to discover an optimal sequence of actions in a decision-making problem and show that a trained reinforcement learning agent can significantly outperform other optimization techniques like a greedy strategy or simulated annealing. The use of graph neural networks to encode the policy of the agent enables generalization to diagrams much bigger than seen during the training phase.

**Recording:**https://youtu.be/jVu-7MBImvs

**Joint-Work With:**Florian Marquardt

**Wednesday January 17th: Reinforcement Learning Based Quantum Circuit Optimization via ZX-Calculus**

**Speaker:**Jan Nogué Gómez (Qilimanjaro Quantum Tech)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Spain/Netherlands

**Abstract:**We propose a novel Reinforcement Learning (RL) method for optimizing quantum circuits using the graph-like representation of a ZX-diagram. The agent, trained using the Proximal Policy Optimization (PPO) algorithm, employs Graph Neural Networks to approximate the policy and value functions. We test our approach for two differentiated circuit size regimes of increasing relevance, and benchmark it against the best-performing ZX-calculus based algorithm of the PyZX library, a state-of-the-art tool for circuit optimization in the field. We demonstrate that the agent can generalize the strategies learned from 5-qubit circuits to 20-qubit circuits of up to 450 Clifford gates, with enhanced compressions with respect to its counterpart while remaining competitive in terms of computational performance.

**Recording:**https://youtu.be/PwqKvMNVzj0

**Joint-Work With:**Jordi Riu, Gerard Vilaplana, Artur Garcia-Saez, and Marta P. Estarellas

**Wednesday January 24th: Multi-Agent Blind Quantum Computation without Universal Cluster States**

**Speaker:**Shuxiang Cao (University of Oxford)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**Blind quantum computation (BQC) protocols enable quantum algorithms to be executed on third-party quantum agents while keeping the data and algorithm confidential. The previous proposals for measurement-based BQC require preparing a highly entangled cluster state. In this paper, we show that such a requirement is not necessary. Our protocol only requires pre-shared Bell pairs between delegated quantum agents, and there is no requirement for any classical or quantum information exchange between agents during the execution. Our proposal requires fewer quantum resources than previous proposals by eliminating the need for a universal cluster state.

**Recording:**https://youtu.be/xFihqZ5cIZ0

**Wednesday January 31st: Flow-Preserving ZX-calculus Rewrite Rules for Optimisation and Obfuscation**

**Speaker:**Tommy McElvanney (University of Birmingham)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**In the one-way model of measurement-based quantum computation (MBQC), computation proceeds via measurements on a resource state. So-called flow conditions ensure that the overall computation is deterministic in a suitable sense, with Pauli flow being the most general of these. Computations, represented as measurement patterns, may be rewritten to optimise resource use and for other purposes. Such rewrites need to preserve the existence of flow to ensure the new pattern can still be implemented deterministically. The majority of existing work in this area has focused on rewrites that reduce the number of qubits, yet it can be beneficial to increase the number of qubits for certain kinds of optimisation, as well as for obfuscation.

In this work, we introduce several ZX-calculus rewrite rules that increase the number of qubits and preserve the existence of Pauli flow. These rules can be used to transform any measurement pattern into a pattern containing only (general or Pauli) measurements within the XY-plane. We also give the first flow-preserving rewrite rule that allows measurement angles to be changed arbitrarily, and use this to prove that the ‘neighbour unfusion’ rule of Staudacher et al. preserves the existence of Pauli flow. This implies it may be possible to reduce the runtime of their two-qubit-gate optimisation procedure by removing the need to regularly run the costly gflow-finding algorithm.

**Recording:**https://youtu.be/rKbtnOgzKZQ

**Joint-Work With:**Miriam Backens

**Wednesday February 7th: Graphical Symplectic Algebra**

**Speaker:**Robert Booth (University of Edinburgh)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**We give complete presentations for the dagger-compact props of affine Lagrangian and coisotropic relations over an arbitrary field. This provides a unified family of graphical languages for both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser quantum circuits. To this end, we present affine Lagrangian relations by a particular class of undirected coloured graphs. In order to reason about composite systems, we introduce a powerful scalable notation where the vertices of these graphs are themselves coloured by graphs. In the setting of stabiliser quantum mechanics, this scalable notation gives an extremely concise description of graph states, which can be composed via ``phased spider fusion.'' Likewise, in the classical mechanical setting of electrical circuits, we show that impedance matrices for reciprocal networks are presented in essentially the same way.

**Recording:**https://youtu.be/QJcEeZsL2S8

**Joint-Work With:**Titouan Carette and Cole Comfort

**Wednesday February 14th: VyZX: Formal Verification of a Graphical Quantum Language**

**Speaker:**Ben Caldwell (University of Chicago)

**Time:**9 - 10 am CT = 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs, particularly for process theories which represent programs using graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to Verify the ZX-calculus, a graphical language for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph’s semantic interpretation. We show how inductive graphs in VyZX are used to prove the correctness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. VyZX integrates easily with the proof engineer’s workflow through visualization and automation.

**Recording:**https://youtu.be/5cwd9u8jivo

**Joint-Work With:**Adrian Lehmann, Bhakti Shah, and Robert Rand

**Wednesday February 28th: Fault-Tolerant Complexes**

**Speaker:**Yehua Liu (PsiQuantum)

**Time:**7 - 8 am PST = 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**Fault-tolerant complexes describe surface-code fault-tolerant protocols from a single geometric object. We first introduce fusion complexes that define a general family of fusion-based quantum computing (FBQC) fault tolerant quantum protocols based on surface codes. We show that any 3-dimensional cell complex where each edge has four incident faces gives a valid fusion complex. This construction enables an automated search for fault tolerance schemes, allowing us to identify 627 examples within a moderate search time. We implement this using the open-source software tool Gavrog and present threshold results for a variety of schemes, finding fusion networks with higher erasure and Pauli thresholds than those existing in the literature. We then define more general structures we call fault-tolerant complexes that provide a homological description of fault tolerance from a large family of low-level error models, which include circuit-based computation, floquet-based computation, and FBQC with multi-qubit measurements. This extends the applicability of homological descriptions of fault tolerance, and enables the generation of many new schemes which have not been previously identified. We also define families of fault-tolerant complexes for color codes and 3d single-shot subsystem codes, which enables similar constructive methods, and we present several new examples of each.

**Joint-Work With:**Hector Bombin, Chris Dawson, Terry Farrelly, Naomi Nickerson, Mihir Pant, Fernando Pastawski, and Sam Roberts

**Wednesday March 6th: Enriching Diagrams with Algebraic Operations**

**Speaker:**Alejandro David Villoria Gonzalez (Leiden Institute of Advanced Computer Science)

**Time:**10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands

**Abstract:**In this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the condition that this monad is monoidal and affine, we construct an adjunction between symmetric monoidal categories and symmetric monoidal categories enriched over algebras for the monad. This allows us to devise an extension, and its semantics, of the ZX-calculus with probabilistic choices by freely enriching over convex algebras, which are the algebras of the finite distribution monad. We show how this construction can be used for diagrammatic reasoning of noise in quantum systems.

**Joint-Work With:**Henning Basold and Alfons Laarman

**Wednesday March 13th: Completeness of Qufinite ZXW Calculus, a Graphical Language for Mixed-Dimensional Quantum Computing**

**Speaker:**Quanlong Wang (Quantinuum)

**Time:**10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**Finite-dimensional quantum theory serves as the theoretical foundation for quantum information and computation based on 2-dimensional qubits, d-dimensional qudits, and their interactions. The qufinite ZX calculus has been used as a framework for mixed-dimensional quantum computing; however, it lacked the crucial property of completeness, which ensures that the calculus incorporates a set of rules rich enough to prove any equation. The ZXW calculus is a complete language for qudit quantum computing with applications previously unreachable solely with the ZX or ZW calculus. In this paper, we introduce the qufinite ZXW calculus, a unification of all qudit ZXW calculi in a single framework for mixed-dimensional quantum computing. We provide a set of rewrite rules and a unique normal form that make the calculus complete for finite-dimensional quantum theory. This work paves the way for the optimization of mixed dimensional circuits and tensor networks appearing in different areas of quantum computing including quantum chemistry, compilation, and quantum many-body systems.

**Joint-Work With:**Boldizsár Poór

**Wednesday March 20th: Teaching Small Transformers to Rewrite ZX Diagrams**

**Speaker:**Richie Yeung (Quantinuum, University of Oxford)

**Time:**10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**ZX calculus is a graphical language for reasoning about linear maps. Maps are represented as graphs, and reasoning amounts to graph rewrites. The main applications of ZX calculus are in quantum computation. We train small transformers to simplify ZX graphs, i.e. perform resource optimisation of quantum circuits. Preliminary experiments show that transformers can be trained to simplify CNOT and Clifford circuits with high accuracy. These are the simplest kinds of ZX graphs, in the sense that there exists an efficient rewrite strategy. We also show evidence that transformers learn to simplify the more complex Clifford + T graphs, for which in general there does not exist an efficient simplification algorithm.

**Joint-Work With:**Konstantinos Meichanetzidis, Alexandre Krajenbrink, and François Charton

**Wednesday March 27th: Minimal Equational Theories for Quantum Circuits**

**Speaker:**Alexandre Clément (Université Paris-Saclay)

**Time:**10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm France/Netherlands

**Abstract:**We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that a multi-control 2π rotation is nothing but the identity. Our work improves on the recent complete equational theories for quantum circuits, by getting rid of several rules including a fairly unpractical one. One of our main contributions is to prove the minimality of the equational theory, i.e. none of the rules can be derived from the other ones. More generally, we demonstrate that any complete equational theory on quantum circuits (when all gates are unitary) requires rules acting on an unbounded number of qubits. Finally, we also simplify the complete equational theories for quantum circuits with ancillary qubits and/or qubit discarding.

**Joint-Work With:**Noé Delorme and Simon Perdrix

## Fall 2023 Schedule

**Monday October 2nd: Every Clifford ZX-Diagram is a Quantum Error Correcting Code**

**Speaker:**Alex Townsend-Teague (Freie Universität Berlin)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**Floquet codes are a recently(-ish!) discovered type of quantum error correction code. Operationally, they work by repeatedly measuring multi-qubit Pauli operators, and thus can be thought of as generalising stabilizer codes. However, they have the defining property that representatives of logical Pauli operators in a Floquet code are dynamic - they change over time. In this talk, we will consider the following perspective, which unifies stabilizer and Floquet codes: every Clifford ZX-diagram is a quantum error correcting code. We will introduce tools needed to understand this view and discuss its applications.

**Recording:**https://www.youtube.com/watch?v=pP1DaKxlC_8

**Joint-Work With:**Julio Magdalena de la Fuente and Markus Kesselring

**Monday October 9th: The ZX Seminar Orientation**

**Chaired by:**John van de Wetering (University of Amsterdam)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Monday October 16th: Speedy Contraction of ZX Diagrams with Triangles via Stabiliser Decompositions**

**Speaker:**Mark Koch (Quantinuum)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**Recent advances in classical simulation of Clifford+T circuits make use of the ZX calculus to iteratively decompose and simplify magic states into stabiliser terms. We improve on this method by studying stabiliser decompositions of ZX diagrams involving the triangle operation. We show that this technique greatly speeds up the simulation of quantum circuits involving multi-controlled gates which can be naturally represented using triangles. We implement our approach in the QuiZX library and demonstrate a significant simulation speed-up (up to multiple orders of magnitude) for random circuits and a variation of previously used benchmarking circuits. Furthermore, we use our software to contract diagrams representing the gradient variance of parametrised quantum circuits, which yields a tool for the automatic numerical detection of the barren plateau phenomenon in ansätze used for quantum machine learning. Compared to traditional statistical approaches, our method yields exact values for gradient variances and only requires contracting a single diagram. The performance of this tool is competitive with tensor network approaches, as demonstrated with benchmarks against the quimb library.

**Recording:**https://youtu.be/8L6jqiNg9iM

**Joint-Work With:**Richie Yeung and Quanlong Wang

**Monday October 23rd: On the Architecture-Aware Synthesis of Pauli Polynomials**

**Speaker:**David Winderl (Technical University of Munich)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Germany

**Abstract:**The synthesis of quantum circuits from so-called Pauli-Polynomials in the ZX Calculus facilitates quantum circuit optimization. In this work, we will develop three algorithms that can perform this task in an architecture-aware fashion. On top, we develop an architecture-aware synthesis method for synthesizing Clifford-Tableaus. Our results show an increase in the Reduction of CNOT-Gates for larger circuits for both Clifford circuits and circuits described by Pauli-Polynomials, which outlines the capabilities of architecture-aware synthesis in the circuit optimization realm.

**Recording:**https://youtu.be/V8dlZgSQYiU

**Joint-Work With:**Qunsheng Huang, Arianne Meijer-van de Griend, and Richie Yeung

**Monday October 30th: Light-Matter Interaction in the ZXW Calculus**

**Speaker:**Boldizsár Poór (Quantinuum)

**Time:**9 - 10 am EDT = 1 - 2 pm UK = 2 - 3 pm Netherlands

**Abstract:**In this paper, we develop a graphical calculus to rewrite photonic circuits involving light-matter interactions and non-linear optical effects. We introduce the infinite ZW calculus, a graphical language for linear operators on the bosonic Fock space which captures both linear and non-linear photonic circuits. This calculus is obtained by combining the QPath calculus, a diagrammatic language for linear optics, and the recently developed qudit ZXW calculus, a complete axiomatisation of linear maps between qudits. It comes with a 'lifting' theorem allowing to prove equalities between infinite operators by rewriting in the ZXW calculus. We give a method for representing bosonic and fermionic Hamiltonians in the infinite ZW calculus. This allows us to derive their exponentials by diagrammatic reasoning. Examples include phase shifts and beam splitters, as well as non-linear Kerr media and Jaynes-Cummings light-matter interaction.

**Recording:**https://youtu.be/nOli0jB2hoY

**Joint-Work With:**Giovanni de Felice, Razin A. Shaikh, Lia Yeh, Quanlong Wang, and Bob Coecke

**Monday November 6th: Unifying Flavors of Fault Tolerance with the ZX Calculus**

**Speaker:**Fernando Pastawski (PsiQuantum)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Germany/Netherlands

**Abstract:**There are several models of quantum computation which exhibit shared fundamental fault-tolerance properties. This article makes commonalities explicit by presenting these different models in a unifying framework based on the ZX calculus. We focus on models of topological fault tolerance – specifically surface codes – including circuit-based, measurement-based and fusion-based quantum computation, as well as the recently introduced model of Floquet codes. We find that all of these models can be viewed as different flavors of the same underlying stabilizer fault-tolerance structure, and sustain this through a set of local equivalence transformations which allow mapping between flavors. We anticipate that this unifying perspective will pave the way to transferring progress among the different views of stabilizer fault-tolerance and help researchers familiar with one model easily understand others.

**Joint-Work With:**Hector Bombin, Daniel Litinski, Naomi Nickerson, and Sam Roberts

**Monday November 13th: Causal Flow Preserving Optimisation of Quantum Circuits in the ZX-Calculus**

**Speaker:**Calum Holker (University of Oxford)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**Optimising quantum circuits to reduce physical implementation resources is crucial, especially in the context of near term hardware, which is limited by quantum volume. This paper aims to minimise T-count and two-qubit gate count by building on ZX-calculus-based circuit optimisation strategies. By translating a circuit into a ZX-diagram it can be simplified before being extracted back into a circuit. We assert that simplifications preserve a graph-theoretic property called causal flow. This has the advantage that qubit lines are well defined throughout simplification, permitting a trivial extraction procedure and in turn enabling the calculation of an individual transformation's impact on the resulting circuit. A general algorithm for a decision strategy is introduced, inspired by the heuristic based method of Staudacher et. al. (2022). Also, both phase teleportation and the neighbour unfusion rule are generalised. In particular allowing unfusion of multiple neighbours is shown to lead to significant improvements in optimisation. When run on a set of benchmark circuits, the algorithm developed reduces the two qubit gate count by an average of 19.6%, beating both the previous best ZX-based strategy (14.2%) as well as the previous best non-ZX strategy (18.9%). This lays the foundation for improvements such as more advanced decision models.

**Recording:**https://youtu.be/9wO_-QcSAaM

**Joint-Work With:**Aleks Kissinger

**Monday November 20th: ZXLive - An Interactive GUI for the ZX Calculus**

**Speaker:**Razin A. Shaikh (University of Oxford & Quantinuum)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**ZXLive is a user-friendly, interactive tool designed for reasoning with the ZX calculus. It offers a simple interface to draw ZX diagrams or import them from various file formats. Once you have your diagram, switch to proof mode where you can easily apply the ZX rules and construct proofs. The tool supports exporting proofs to Tikzit for adding it into papers. These proofs can also be saved as lemmas, which can be used later as rewrite rules in other proofs. With support for custom rewrites, you can add new rules to ZXLive that are relevant for your current project. Beyond the vanilla ZX calculus, ZXLive supports the generators and rewrite rules of ZH, ZW, and ZXW calculi.

ZXLive is available as an open-source project on GitHub: https://github.com/Quantomatic/zxlive. Under the hood, it is powered by PyZX, which is an open-source python library for ZX. Along with being a useful tool for ZX practitioners, ZXLive is also a great educational tool for learning and experimenting with the ZX calculus.

**Recording:**https://youtu.be/J--c2q-KOc8

**Monday November 27th: A ZX-Calculus Approach to Concatenated Graph Codes**

**Speaker:**Zipeng Wu (Hong Kong University of Science and Technology)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**Quantum Error-Correcting Codes (QECCs) are vital for ensuring the reliability of quantum computing and quantum communication systems. Among QECCs, stabilizer codes, particularly graph codes, have attracted considerable attention due to their unique properties and potential applications. Concatenated codes, which combine multiple layers of quantum codes, offer a powerful technique for achieving high levels of error correction with a relatively low resource overhead. In this paper, we examine the concatenation of graph codes using the powerful and versatile graphical language of ZX-calculus. We establish a correspondence between the encoding map and ZX-diagrams, and provide a simple proof of the equivalence between encoding maps in the Pauli X basis and the graphic operation "generalized local complementation" (GLC) as previously demonstrated in [J. Math. Phys. 52, 022201]. Our analysis reveals that the resulting concatenated code remains a graph code only when the encoding qubits of the same inner code are not directly connected. When they are directly connected, additional Clifford operations are necessary to transform the concatenated code into a graphcode, thus generalizing the results in [J. Math. Phys. 52, 022201]. We further explore concatenated graph codesin different bases, including the examination of holographic codes as concatenated graph codes. Our findings showcase the potential of ZX-calculus in advancing the field of quantum error correction.

**Recording:**https://youtu.be/mbqx0OudY5c

**Joint-Work With:**Song Cheng and Bei Zeng

**Monday December 4th: Graphical Algebra and the Connection to Graphical Languages for Quantum Circuits**

**Speaker:**Cole Comfort (MOCQUA team, LORIA, Université de Lorraine)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**The ZX-calculus is a family of graphical languages used to reason about fragments of complex-valued matrices under the bilinear tensor product. However, by restricting oneself to the phase-free fragment of the ZX-calculus, one obtains a graphical calculus for reasoning about linear subspaces over the integers modulo p under the direct sum. In order to expose this correspondence, I will review the scalable notation and discuss how this allows one to perform basic constructions in linear algebra using the ZX-calculus. I will also discuss how one can capture more general notions of subspaces by adding more generators to the ZX-calculus. In particular, I will discuss how extending this correspondence between the phase-free ZX-calculus and linear subspaces over Z/pZ has can be applied to stabilizer codes as well as SAT solving. I will also discuss open problems which may be interesting to the ZX-calculus community.

**Recording:**https://youtu.be/80rx6LzWCWo

**Monday December 11th: Graphical CSS Code Transformation Using ZX Calculus**

**Speaker:**Jiaxin Huang (The University of Hong Kong)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands

**Abstract:**In this work, we present a generic approach to transform CSS codes by building upon their equivalence to phase-free ZX diagrams. Using the ZX calculus, we demonstrate diagrammatic transformations between encoding maps associated with different codes. As a motivating example, we give explicit transformations between the Steane code and the quantum Reed-Muller code, since by switching between these two codes, one can obtain a fault-tolerant universal gate set. To this end, we propose a bidirectional rewrite rule to find a (not necessarily transversal) physical implementation for any logical ZX diagram in any CSS code.

Then we focus on two code transformation techniques: code morphing, a procedure that transforms a code while retaining its fault-tolerant gates, and gauge fixing, where complimentary codes can be obtained from a common subsystem code (e.g., the Steane and the quantum Reed-Muller codes from the [[15,1,3,3]] code). We provide explicit graphical derivations for these techniques and show how ZX and graphical encoder maps relate several equivalent perspectives on these code-transforming operations.

**Recording:**https://youtu.be/ZhfQxdjodNs

**Joint-Work With:**Sarah Meng Li, Lia Yeh, Aleks Kissinger, Michele Mosca, and Michael Vasmer

**Monday December 18th: The Zeta Calculus**

**Speaker:**Nicklas Botö (Chalmers University of Technology)

**Time:**9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Sweden

**Abstract:**Working from the internal type theory of compact closed symmetric monoidal categories, we extend the linear multiplicative typed λ-calculus with observable structures to obtain a programming language suitable for the categorical view of quantum computation. At the current stage of development, the phase groups and cocommutative comonoids of observable structures are embedded into the typing and structural rules of the language to provide basis-dependent non-linearity as well as a notion of rotational computing. We show that this language provides novel programming techniques and ways of constructing categorical quantum programs, notably in the ZX-calculus. The generality of the categorical definition of the language allows it to be instantiated in any model of compact closed symmetric monoidal categories with any number of observable structures, or internal cocommutative comonoids. We hope that this creates new avenues in which to explore what quantum programming might be, and which theories it might describe.

**Recording:**https://youtu.be/iUHEy3PZCso

**Joint-Work With:**Fabian Forslund