LIQCS 2026

We introduce a theory for computational control, consisting of eight naturally interpretable equations. Adding these to a prop of base circuits constructs controlled circuits, borne out in examples of reversible Boolean circuits and quantum circuits. We prove that this syntactic construction semantically corresponds to taking the free rig category on the base prop.

We use the Chu construction to functorially build BV-categories from duoidal categories, demonstrating that candidate models of BV-logic can be cofreely constructed from a fragment of a model of Guglielmi’s sequencing operator. By using this construction to show that the strong Hyland envelope is a BV-category, we find a way to build a canonical model of spatio-temporal relationships between agents in spacetime from any symmetric monoidal category. The concrete physical interpretation of spacetime events in this model as intervention-context pairs resolves deficiencies in previous attempts to give a general categorical semantics to higher-order quantum operations - in particular, those which are unitary.

Completeness for a quantum-circuit fragment answers only part of the equational story. It tells us that every valid identity can be derived, but it does not distinguish genuine algebraic laws from equations that merely encode structural symmetry, nor does it say whether the surviving axioms are independent. We therefore revisit six near-Clifford fragments in a PROP setting, where wire permutations are ambient structure rather than fragment-specific axioms, and obtain smaller complete presentations for qubit Clifford, real Clifford, CNOT-dihedral, bounded-wire Clifford+T, bounded-wire Clifford+CS, and qutrit Clifford.

Across the six fragments, the PROP reformulation exposes a smaller algebraic core while still leaving nontrivial derivations to recover laws that were previously explicit. The reduced PROP presentations for qubit Clifford, real Clifford, and CNOT-dihedral are minimal; those for Clifford+T and Clifford+CS are minimal at low arity but leave one further wire layer to settle; and qutrit Clifford is minimal up to two qutrit wires, leaving only a single ternary braid relation unresolved.

We introduce the L-S-!-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (ILL). These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the L-S-!-calculus as an extension of the L-S-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalisation, and an introduction property—as well as preserve the expressiveness of the original L-S-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a quantum programming language grounded in linear logic.

This is an extended abstract of arXiv:2504.12128.

We present lambdaB, a quantum‐control lambda‐calculus that refines previous basis-sensitive systems by allowing abstractions to be expressed with respect to arbitrary—possibly entangled—bases. Each abstraction and let-construct is annotated with a basis, and a new basis-dependent substitution governs the decomposition of value distributions. These extensions preserve the expressive power of earlier calculi while enabling finer reasoning about programs under basis changes. A realisability semantics connects the reduction system with the type system, yielding a direct characterisation of unitary operators and ensuring safety by construction. From this semantics we derive a validated family of typing rules, forming the foundation of a type-safe quantum programming language. We illustrate the expressive benefits of lambdaB through examples such as Deutsch’s algorithm and quantum teleportation, where basis-aware typing captures classical determinism and deferred-measurement behaviour within a uniform framework.

Based on the submitted paper arXiv:2510.18542v1.

The standard circuit model used to describe quantum operations is well understood, but is unable to represent a class of higher-order operations that feature quantum control and an indefinite causal ordering of higher order input. In particular, the quantum switch, which orders two unitary operations depending on the value of a control qubit, has been realized physically.

Alongside this, notions of control flow are well studied in proof theory, in particular using Linear Logic. LL also presents multiple features that make it an attractive starting point to study quantum computing from a logical angle, such as restricted duplication and discarding of formulae.

In this work in progress, we introduce a modified version of Intuitionistic Multiplicative Additive Linear Logic alongside a semantic for it that represents higher order computation. This logic presents cut elimination, and proofs evaluating to multiple known higher order processes, as well as universality for unitaries.

Polylogarithmic time delineates a relevant notion of feasibility on several classical computational models such as Boolean circuits or parallel random access machines. As far as the quantum paradigm is concerned, this notion yields the complexity class FBQPOLYLOG of functions approximable in polylogarithmic time with a quantum random access Turing machine. We introduce a quantum programming language with first-order recursive procedures, which provides the first programming language-based characterization of FBQPOLYLOG. Each program computes a function in FBQPOLYLOG (soundness) and, conversely, each function of this complexity class is computed by a program (completeness). We also provide a compilation strategy from programs to uniform families of quantum circuits of polylogarithmic depth and polynomial size, whose set of computed functions is known as QNC, and recover the well-known separation result FBQPOLYLOG ⊊ QNC.

While quantum hardware remains limited, hybrid quantum-classical algorithms with complex control structures, including unbounded loops, are emerging, posing new challenges for program analysis: the accurate estimation of resource consumption of a given program is needed. In this work, we answer this challenge with the first static analysis solution for reasoning about the resources — termination or cost — of hybrid quantum programs with unbounded loops. Towards that end, we introduce hybrid path-sums, a symbolic representation of possible executions of a quantum program. A generic strategy for determining termination and expected resource consumption via loop invariants is also proposed. Finally, a prototype of this solution is implemented in Haskell. This work is the first step toward the design of a complete static resource analysis tool for hybrid quantum programs with unbounded loops, essential for the development of real-world quantum computing. This extended abstract illustrates fully developed results without expanding on the technicalities.

The stabiliser fragment of quantum theory is a foundational building block for quantum error correction, and hence for the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal, and complete denotational semantics for stabiliser operations, including measurement, classically controlled Pauli operators, and affine classical computation; supporting an explicit treatment of quantum error-correcting codes. We interpret stabiliser operations as affine relations over finite fields, yielding a semantics that reflects the algebraic structure underlying stabiliser quantum error correction. Because stabiliser quantum mechanics has a well-behaved algebraic structure, our relational semantics is conceptually transparent and computationally tractable when compared to standard denotational models for general quantum programs.

We demonstrate the resulting semantics by describing a small, low-level assembly language for stabiliser programs with fully-abstract denotational semantics.

We present a complete set of rewrite rules for multi-qudit Clifford circuits, where qudit denotes a d-level quantum system with d an odd prime. Completeness means that any two Clifford circuits representing the same linear map can be transformed into each other using these rules. In total, there are 19 Clifford relations, each involving at most three qudits and admitting an intuitive interpretation.

Our approach leverages the isomorphism between the symplectic group Sp(2n,Zd) and the quotient of the Clifford group by the Pauli group. We first derive a complete set of symplectic relations for Sp(2n, Zd), and then lift them to Clifford relations by incorporating Pauli corrections. To do this, we introduce a symplectic normal form that captures the stabiliser tableau of a Clifford operator and is unique up to Pauli correction. This simplification enables a streamlined derivation of a complete set of 66 relations, which we further compress to 18 symplectic relations. Our computations in Sp(2n,Zd) are formalised in the Agda proof assistant, providing a machine-verified proof of correctness.

We introduce Graphical Algebraic Geometry (GAG), a family of diagrammatic languages extending the Graphical Linear Algebra program. We construct several languages within this family and prove that they are universal and complete for the corresponding (co)span semantics of commutative algebras and affine varieties. This framework provides clear graphical representations of algebraic structures — such as polynomials, ideals, and varieties — enabling intuitive yet rigorous diagrammatic reasoning.

We showcase two practical viewpoints on GAG. First, we show that instances of counting constraint satisfaction problem (#CSP) are recast as rewrite problems of closed diagrams in GAG. This means that deciding rewriteability in GAG is #P-hard, and GAG can be viewed as a complete and compositional rewrite system for networks of polynomial constraints. Second, we characterize the qudit ZH calculus, a diagrammatic language for quantum computation, as an extension of Graphical Algebraic Geometry. This establishes the correspondence that Graphical Algebraic Geometry is to the ZH calculus what Graphical Linear Algebra is to the ZX calculus. Using this construction, we show that computing amplitudes in qudit ZH requires only a constant number of queries to a GAG oracle. Finally, using a catalysis-style argument, we leverage the completeness of GAG to solve the open problem of finding a complete set of rewrite rules for the Qudit ZH calculus.

We propose a structural perspective on completeness for equational theories of quantum computing, observing that a large class of equations arise from ambient computational structure, notably that of rig categories. Once this structure is accounted for, the remaining equations are few and admit a clear geometric interpretation. We make this perspective concrete by giving a constructive and generic description of the equational theory for unitary matrices, explicating generic normal forms for unitaries, and use this to derive a recipe to obtain complete equational theories for unitaries with any generator, as long as we have completeness on 2-dimensional systems and enough structure.

We show that the category OS of operator spaces, with complete contractions as morphisms, is locally countably presentable and a model of Intuitionistic Linear Logic in the sense of Lafont. We then describe a model of Classical Linear Logic, based on OS, whose duality is compatible with the Heisenberg-Schrödinger duality of quantum theory. We explore connections between the Haagerup tensor product on OS and BV-logic and we also show that OS provides a good setting for studying pure state and mixed state quantum information, the interaction between the two, and even higher-order quantum maps such as the quantum switch. This work was published in LICS’25 [1]. A preprint with many omitted proofs is available [2] and we also have a detailed companion paper [3] that provides a proof of the local presentability of OS and proofs that establish other important categorical properties of OS.

We describe a categorical model of MALL (Multiplicative Additive Linear Logic) inspired by the Heisenberg-Schrödinger duality of finite-dimensional quantum theory. Proofs of formulas with positive logical polarity correspond to CPTP (completely positive trace-preserving) maps in our model, i.e. the quantum operations in the Schrödinger picture, whereas proofs of formulas with negative logical polarity correspond to CPU (completely positive unital) maps, i.e. the quantum operations in the Heisenberg picture. The mathematical development is based on noncommutative geometry and finite-dimensional von Neumann (co)algebras, which can be defined as special kinds of (co)monoid objects internal to the category of finite-dimensional operator spaces.

We present a different vision on the foundations of quantum computing, which we believe should be based on the principles of noncommutative geometry. This requires a higher level of abstraction than is common in quantum computing. In particular, working with infinite dimensional systems is necessary. We argue why this level of abstraction is necessary to make the next step in quantum computing, and give an overview of applications of noncommutative structures in quantum information science and in the denotational semantics of quantum programming languages and logics in particular.

Quantum Bayesian networks [Henson, Lal, and Pusey, 2014] provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl’s Bayesian networks [Pearl, 1986]—prominent graphical models for classical probabilistic reasoning and inference. This extended abstract reports on work [Di Guardia, Ehrhard, and Faggian, 2026] which brings compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems.

Quantum computation provides a quadratic speedup for the inference process in Bayesian networks. We propose an effective methodology to compile functional programs to quantum circuits, via Bayesian networks. While in this talk we will mainly deal with the first order fragment, our technique can scale to the higher-order case, covering languages featuring recursion, and complex evaluation mechanisms, such as call-by-push-value. The main technical ingredient is the introduction of a parallel version of the Krivine Abstract Machine, that is able to build the Bayesian network while evaluating the program. Moreover, we propose some optimizations that reduce the size of the quantum circuit produced as output by the machine.

The development of quantum communication protocols sparked the interest in quantum extensions of process calculi. The prominent approaches, however, are still based on probabilistic models, which are inadequate for the quantum case, as they do not capture the observational limitations of quantum theory. In Physics, probabilistic quantum systems are not represented with probabilities, but with density operators. By lifting this concept to the Computer Science setting, we introduce Operator Distributions: they employ density operators as weights, just like probability distributions use real numbers. We give semantics to quantum protocols in a natural way, as an LTS of operator distributions, guaranteeing that only physically accessible information about the systems are represented. Moreover, these “quantum” distributions pave the way for symbolic verification of protocols whose behaviour depends on an unknown initial state: instead of considering infinitely-many LTSs, one for each possible initialization, we can build a single symbolic LTS and prove properties on it.

In quantum probability, the category of C-algebras and completely positive unital (cpu) maps is a well-established setting. However, its classical side, given by commutative C-algebras, does not contain all regular conditional probabilities, a central concept in classical probability. This shortcoming is due to the inherent topological nature of C*-algebras, which ties them to continuous rather than measurable structures.

To address this, we investigate what quantum measurable spaces should be, by establishing equivalences between special classes of C*-algebras and cpu maps and categories of measurable spaces with Markov kernels. Moreover, our operator-algebraic analysis equips these structures with a generalized notion of Markov kernels, realized as POVMs.

Ultimately, we obtain a categorical framework in which both classical and quantum probability coexist, and the classical side has regular conditional probabilities.

Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.

In contrast to a classical bit, which can only take the value 0 or 1, its quantum counterpart—a qubit—can exist in a superposition of $0$ and $1$. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community.

Programming languages with quantum control typically restrict the target of quantum control to unitary operations; as a consequence, they cannot express the quantum SWITCH, which applies to quantum channels—the broader class that includes measurements. There are some proposals of languages with both measurement and quantum control, but these languages cannot describe the quantum SWITCH and suffer from an ill-behavedness issue of the semantics.

This paper introduces a novel quantum programming language with both quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis, we identify the source of the ill-behavedness as the correspondence problem: a lack of coordination between the then- and else-branches of a quantum conditional branching. We address this with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.

This paper introduces the hybrid quantum language with general recursion Hyrql, which is driven towards resource-analysis. By design, Hyrql does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity. It also satisfies standard properties of programming languages, such as progress, subject reduction and confluence.

Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of Hyrql programs with the size of the corresponding quantum circuits. We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao’s Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

A complete version is available online at https://arxiv.org/abs/2510.20452.

In this work, we aim to give hybrid quantum computation a concrete denotational semantics by modelling it as a computational effect added to a purely classical language. To this end, we introduce the finite quantum instruments monad, which can be understood as a generalisation to quantum evolutions of the finite distribution monad, cleanly separating the classical and quantum parts of a program’s semantics. Going beyond the case of finitely supported instruments, we sketch ongoing work in extending it to measurable spaces, in analogy with the Giry monad, and to directed-complete partial orders (DCPOs) to allow modelling of programs that may diverge, in analogy with the probabilistic powerdomain monad.

We develop a semantic framework for approximate quantum computation based on spectral transformations of quantum states. We introduce spectral quantum spaces, extending projective quantum state spaces by incorporating effects generated via functional calculus in the spectrum of observables and closed under convex combinations and multiplication of commuting effects. Building on this, we define polynomial spectral signal-state relations, where observable evaluations of parameterized states are polynomial functions of the parameters.

This framework separates structural (spectral) and computational (polynomial) aspects of quantum processes, and provides a natural setting for reasoning about approximation. As a case study, we formalize the Bravyi-Kitaev 5-qubit magic state distillation protocol as a morphism in the category of polynomial spectral signal-state relations. In this formulation, the protocol acts as a rational transformation on spectral parameters, arising from polynomial evaluation followed by normalization.

Time-dependent processes are often described in terms of machines with an internal state which is updated as time evolves. However, from the perspective of an external observer, two such processes can produce the same behaviour, even when their internal states differ. We introduce a semantic construction which equates processes when they exhibit the same infinite external behaviour, as determined by all finite observations. Our construction is defined over any preorder-enriched monoidal category with a suitable notion of discarding. This provides a unified framework for partial, non-deterministic, probabilistic, and quantum processes evolving in space and time.

In this extended abstract we shall focus on the case of stateful quantum processes.

We write down a series of basic laws for (strict) higher-order circuit diagrams. More precisely, we define higher-order circuit theories in terms of: (a) nesting, (b) temporal and spatial composition, and (c) equivalence between lower-order bipartite processes and higher-order bipartite states. In category-theoretic terms, these laws are expressed using enrichment and cotensors in symmetric polycategories, along with a frobenius-like coherence between them. We describe how these laws capture the salient features of higher-order quantum theory, and discover an upper bound for higher-order circuits: any higher-order circuit theory embeds into the theory of strong profunctors.

Sequential and concurrent models of classical or quantum computation, such as Turing machines and circuits, describe computation as state changes over time. However, models like the Lambda calculus use higher-order operations on functions and are not immediately reducible to a sequence of state transformations. Physically, this corresponds to considering transformations of transformations, forming the basis of Higher-Order Quantum Theory. Here, quantum channels become inputs, enabling “second-order” gates that map channels to channels. This extends recursively, creating a hierarchy of higher-order maps (HOMs). We provide an axiomatic framework, analogous to Kraus’ axiomatization of quantum operations, in which we characterize the admissible HOMs. Using the Choi isomorphism, we show that admissible maps lie within a cone of positive operators constrained by linear conditions [1]. Within the hierarchy, some HOMs can be realized as quantum circuits with open slots, while others (e.g., the quantum switch) exhibit an indefinite causal order. We prove a result linking a map’s functional description (i.e., its type) to its causal structure via no-signaling relations, based on the compositional structure of HOMs [2]. We then present a generalization of the higher-order framework to general physical theories, as described by the formalism of Operational Probabilistic Theories (OPTs) [3]. The starting point is to enrich an OPT with the notion of “contraction.” A contraction is a transformation resembling a categorical trace, which extends the compositional structure of the OPT beyond the sequential one and allows us to define the hierarchy of HOMs. We prove that a (convex) OPT admits a contraction if and only if it is endowed with the so-called Choi states and Choi effects. Therefore, within our framework, the higher-order functionality of an OPT is not an extrinsic element but is fully determined by its native compositional structure.

[1] AB, P. Perinotti, Proc. R. Soc. A 475 20180706 (2019) [2] L. Apadula, AB, P. Perinotti, Quantum 8, 1241 (2024) [3] AB, M. Erba, L. Apadula, P.Perinotti (in preparation)

We explore the sense in which the existing constructions for higher-order maps on quantum theory based on causality constraints and compositionality constraints respectively, coincide. More precisely, we construct a functor F : Caus(C) → StProf(C1) from higher-order causal categories to the category of strong profunctors over first-order causal processes that is lax-lax duoidal, full, faithful, and strongly closed whenever C is additive. When C = CP this embedding is furthermore strong on the sequencer for duoidal categories, expressing the possibility to interpret one-way signalling (but not general non-signalling) constraints in terms of the coend calculus for profunctors. We conclude that in so far as compositional constraints can be used to express causality constraints, the profunctorial approach generalises higher-order quantum theory to a construction over general symmetric monoidal categories.