RubberDUQ workshop

Lie Algebra is Process Algebra
— Robin Kaarsgaard (University of Southern Denmark)

Physical quantum processes compose in parallel by adding their energy functions. Two spins coupled along the same axis, a molecule vibrating while its electrons rearrange: each is a sum of contributions acting simultaneously, not a sequence of gates applied one after another. Circuit languages, built entirely on sequential composition, have no primitive for this additive combination. Hamilton gives it one.
Hamilton is a process calculus whose parallel operator is additive combination of quantum evolutions. This addition lives in the Lie algebra of the group of unitaries, and the Lie-Trotter product formula, which recovers any such sum as a limit of ever-finer sequential interleavings, is Hamilton’s operational semantics. Writing a quantum simulation means writing a Hamilton term; compiling it means choosing a refinement level and unrolling the interleaving. The correspondence between the two levels is exact: the semantics is fully abstract, the expressible programs are precisely those with dyadic-rational Pauli coefficients, and the equational theory is complete. We have a full implementation, validated on a quantum chemistry problem with clean first-order Trotter convergence across eight levels of refinement, and Agda proofs that sanity-check the core metatheory. (back ↥)

Guppy & co: quantum programming at Quantinuum
— Seyon Sivarajah (Quantinuum)

Guppy is an advanced quantum programming language embedded in Python, built for production use and running on real quantum hardware. This talk presents the language and its supporting ecosystem at Quantinuum, exploring how ideas from programming language theory meet the practical demands of quantum execution.
Guppy combines familiar imperative syntax with expressive classical control flow, a linear type system and an ownership discipline, enabling modular quantum-classical programs while detecting qubit misuse at compile time. The talk examines the functional foundations beneath this interface and introduces HUGR, a graph-based intermediate representation that brings linear dataflow and classical control flow together for compilation and optimisation. It follows the path from source code to emulation with Selene and execution on Quantinuum hardware.
The talk concludes with work on fault-tolerant programming, including expressing quantum error correction, compiling algorithms into encoded programs, and building reusable algorithm libraries.
(back ↥)

TBD
— Takeshi Tsukada (Chiba University)

TBD (back ↥)

Programming Abstractions for Quantum Computation
— Amr Sabry (Indiana University)

Quantum circuit languages provide an essential description of execution, but a circuit rarely exposes the computational structure that guides program construction. This talk investigates programming abstractions above circuits and asks which parts of a quantum program require a genuinely quantum account.
First, symbolic retrodictive execution maps a class of classically simulatable quantum programs to Boolean constraint problems using partial evaluation. Second, QGAT exposes generate-and-test structure in selected oracle algorithms and provides both classical execution and compilation to Quipper. Third, ENQ expresses finite optimization through choice generation, energy assignment, and minimization, with classical, gate-model, and annealing interpretations. I then consider general-purpose models based on continuations with controlled sharing and on a reversible functional core extended with measurement and Hamiltonian evolution.
Across these examples, a common design principle emerges: preserve ordinary computational structure and isolate the quantum-specific contribution. This separation supports multiple interpretations of a single program and makes opportunities for classical execution explicit. It also exposes the main unresolved question: which compositional language structures characterize the source of quantum computational advantage? (back ↥)

Practical High-level Quantum Programming
— Timon Gehr (ETH Zurich)

A key challenge in quantum software engineering is to make high-level languages and compilers powerful enough that manual circuit construction becomes the exception rather than the rule.
With large-scale fault-tolerant quantum computing on the horizon, structured intermediate representations for hybrid quantum/classical programs are gaining relevance. Measurement feedback with classical feed-forward can reduce resource requirements, so compiler optimizations must operate on a representation that allows them to seamlessly straddle the boundary between quantum and classical operations. Moreover, optimizing structured programs avoids repeatedly optimizing each instance of a gadget in an unrolled circuit.
This creates a natural synergy between high-level quantum programming and hybrid intermediate representations: the precise boundary between classical and quantum operations is a low-level implementation detail best left to automated transformations, and high-level representations preserve programmer intent that can inform these transformations. While transformations on fixed-size quantum circuits are relatively well studied, high-level transformations of hybrid programs remain less explored.
To help meet these challenges, we are developing a compiler stack for efficient execution of Silq programs on fault-tolerant hardware. Our Silq compiler targets our High-level Quantum Intermediate Representation (HQIR), where we perform uncomputation and adjoint synthesis directly on hybrid programs while preserving high-level structure and asymptotic operation counts. I will also present promising preliminary results from our work-in-progress HQIR optimizer and conclude with some of our open questions around quantum semantics based on partial isometries in the context of compiler optimization. (back ↥)

Higher-Order Programs with Indefinite Causal Orders: a Linear Approach to Coherent Control of Quantum Processes
— Kathleen Barsse (Inria Nancy)

Processes with indefinite causal order (ICO), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In this talk, I will present a higher-order quantum functional language that supports processes with ICO and whose linear type system allows quantum control to be well-defined on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. (back ↥)

A Traceless Interaction
— Kostia Chardonnet (Inria Nancy)

In the past decades, a major trend in denotational semantics has been the extension of models to deal with quantitative effects or aspects of computation. This includes, for instance, models of various kinds of probabilistic or quantum programming. An important construction in semantics to build such models is the Int Construction, allowing us to "complete" a monoidal category into a compact closed one. One of the main challenges of that construction is to handle composition properly. In order to do so, the existence of a trace is required in the base category. However, there are many categories where such a trace does not exist, such as measurable spaces and stochastic kernels; or the category of finite dimensional Hilbert spaces and linear maps. In this talk, we propose a refinement of the Int Construction, that allows us to build a *-autonomous category out of a monoidal category, without a trace. (back ↥)

Grover's algorithm and simulation in modern quantum programming language
— Debabrata Ghoshal (Washington Quantum Computing Meetup, DC)

We are investigating Grover's algorithm in modern quantum programming language. Our analysis explores the transition from pure state vectors to density matrices, which is critical for evaluating how real-world noise, such as decoherence and relaxation, impacts algorithm performance.
Specifically, we discuss the definitions, relations, and core concepts related to the density matrix in quantum mechanics, alongside how our present quantum language expresses its types and semantics. Using this density matrix framework, we demonstrate how to run Grover's algorithm and analyze noise (finite temperature) in multi-qubit simulations to obtain success probabilities of Grover's search results. Ultimately, our goal is to build this simulation capability into a future programming language. (back ↥)

Semantics for fault-tolerant quantum compilation
— Robert Booth (University of Oxford)

Fault-tolerant quantum computation requires quantum data to be encoded in highly symmetric error-correcting codes. Computations must then be compiled into physical operations that exploit these symmetries to detect and correct errors, while simultaneously carrying out the desired computation and keeping the resulting overheads under control. As hardware moves towards fault tolerance, we need systematic methods for translating computations into efficient fault-tolerant implementations. Developing these methods will require bringing together research on compilers and quantum error correction. In this talk, I will first outline some of the key problems that a theory of fault-tolerant compilation must address. I will then argue that the field currently lacks a crucial building block familiar from classical compiler design: good semantics for error-correcting (i.e. fault-tolerant) quantum programs. Finally, I will describe two parallel strands of work addressing aspects of this gap. The first, with Alex Rice, Dominik Leichtle, and Kim Worrall, models the interaction between a classical host language and a quantum processor as a computational effect. The second, with Cole Comfort, develops practical denotational semantics for stabiliser (Clifford) quantum programs using symplectic geometry. (back ↥)

Quantum Term Rewrite Systems: Applications to Complexity Analysis
— Thomas Vinet (Inria Nancy)

Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this talk, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time. (back ↥)

Plug and Play: Modular Semantics for Quantum Programming Languages
— Jacob Trevor (University of Glasgow)

The semantics of quantum programming languages can be formalised in many ways. These different semantic styles have different analytical properties, and are sometimes capable of expressing different things. Often, a language must be given a semantics in some relatively more complex terms, because of the inclusion of a particular feature. In this talk, I will present some in-progress work on modularising the semantics of quantum programming languages. This allows us to define the semantics of different fragments of a language in different terms, and bring the fragments together in a way that retains the semantic structure. Doing so can provide material benefits: for example, providing simple decision procedures for the equivalence of some programs, even when the semantics given to the language would require a much more complex approach. This is based off of some ongoing work mechanising the semantics in the Lean theorem prover. (back ↥)

From Cut Ranks to Perfect Tensors: Algebraic Design of Multipartite Entanglement
— Zakaria Dahbi (King's College London)

Absolutely maximally entangled states are important resources for quantum error correction, secret sharing, and quantum networks, but their construction and verification remain difficult for large systems and high local dimensions. In this talk, I will present an algebraic framework for designing and certifying multipartite entanglement using quadratic phase states over finite fields. The key result is that the purity of any subsystem is determined exactly by the rank of a corresponding cut submatrix of a phase matrix. Consequently, verifying maximal entanglement reduces finite-field linear algebra rather than explicit manipulation of exponentially large state vectors. I will then discuss how the Chinese Remainder Theorem decomposes composite-dimensional systems into independent prime-field sectors, yielding additive Rényi-2 entropies and useful obstruction criteria. Finally, I will describe a computational search and certification procedure, including an explicit, absolutely maximally entangled state with 17 parties and local dimension 10001. The results connect multipartite entanglement, graph-state methods, quantum MDS codes, and finite-field rank geometry. (back ↥)

zkFOL: cryptographic certificates for logical validity
— Murdoch Gabbay (Heriot-Watt University)

About three years ago I got interested in how cryptographers use linear algebra to encode (they call this "arithmetise") computation. They encode computation as polynomials, then treat these polynomials as vectors, and using linear algebra and cryptography they are able to prove that a computation was done correctly using a succinct cryptographic certificate. This is called "succinct" or "zero-knowledge" cryptographic proof.
I looked at this use of linear algebra and saw logic. I developed this in a paper and associated exposition

1. Arithmetisation of computation via polynomial semantics for first-order logic, https://eprint.iacr.org/2024/954
2. Cryptographic certificates of validity for trustworthy AI, https://arxiv.org/abs/2606.23768

The upshot of this research is that arbitrary logical validity — that is, actual truth of logical assertions about digital systems describable using logic and polynomial arithmetic — is susceptible to succinct cryptographic proof. I call this "zkFOL", for "zero-knowledge first-order logic", and it is a powerful generalisation of the cryptographer's notion of succinct proof from computation to arbitrary logic. This is extremely powerful.
In collaboration with a cryptographer and a compiler designer, we have produced a prototype compiler which in laboratory tests outperforms the current state of the art cryptographic proof systems by three or four orders of magnitude.
So why do I propose this talk for a workshop on quantum computation? Because zkFOL is yet another way of combining linear algebra with logic and computation. In the spirit of interdisciplinary research, I will present the mathematics and seek correspondences with and insights from the linear algebra used in quantum computation. (back ↥)