Qoreo: Choreographic Programming for Quantum Distributed Systems

AI summary

Overview

Research area: Quantum programming languages and quantum networking — specifically choreographic programming (a global-programming approach from distributed systems) applied to distributed quantum protocols.

Technical level: Intermediate. The paper is a programming-languages theory paper (linear type systems, operational semantics, mechanized proofs) with quantum computing content; readers need some familiarity with types and with basic quantum mechanics (qubits, gates, measurement, entanglement).

Scope in one sentence: Qoreo is a language in which a whole distributed quantum protocol is written as one global choreography and automatically compiled, with machine-checked guarantees of type safety and deadlock freedom, into a network of independent node processes extractable to NetQASM.

What This Paper Is About

Writing a distributed quantum protocol such as teleportation as a set of separate actor processes is repetitive and error-prone: if Alice forgets to send a message, Bob deadlocks, and if Bob expects messages in a different order, he silently computes with wrong values without any runtime error. Qoreo instead lets a programmer write the entire protocol once, from a global viewpoint, in a form that closely resembles the informal circuit diagram of the protocol, and then derives the per-node processes automatically. The goal is to make such protocols easier to write and reason about while guaranteeing that the derived network is well-typed, deadlock-free, and implements the intended quantum operation.

Key Contributions

1. A three-layer language for distributed quantum computing. Qoreo consists of a local quantum language based on the quantum lambda calculus with linear types enforcing the no-cloning principle; a choreographic language combining local quantum computation with inter-actor classical and quantum communication; and a process language describing individual network nodes.

2. A novel linear type system for choreographies, with proved type safety. The paper establishes type safety for the local language (Theorem 3.8) and for the choreographic language (Theorem 4.8), guaranteeing that well-typed programs implement well-defined quantum operations. The authors state this is, to their knowledge, the first integration of a linear type system with choreographies.

3. Endpoint projection (EPP) with soundness and completeness proofs. EPP automatically derives a network of independent processes from any choreography. The paper proves EPP sound (Theorem 6.2) and complete (Theorem 6.5) with respect to the choreographic semantics, yielding as Corollary 6.6 that every well-typed choreography projects to a deadlock-free process network.

4. Full mechanization and a deployment toolchain. All definitions and results in Sections 3, 4, and 5 are fully formalized in Rocq (available on GitHub at github.com/uvm-plaid/qoreo), and the paper provides an extraction pipeline from Rocq to NetQASM for simulation and deployment on quantum network hardware.

Main Findings

• Teleportation becomes one global program. The choreography for quantum teleportation (Figure 3) uses dedicated syntax for entanglement generation (A.a <~> B.b), classical message sending (A.x ~> B.x), and actor-annotated local operations, and the authors argue it bears a striking similarity to the informal circuit description in Figure 1.

• Linear types prevent illegal quantum operations. Qubit references are treated linearly like linear variables: they cannot be duplicated or discarded, blocking programs such as g(q,q) that would violate no-cloning.

• Type safety for both layers. Progress and preservation are proved for the local language (Lemma 3.3 progress, plus substitution, weakening, and inversion lemmas), and type safety is stated for the choreographic language in Theorem 4.8.

• Projection preserves semantics and eliminates deadlock. Because EPP is sound and complete, any reasoning done at the global choreographic level carries over to the projected processes; deadlock freedom of the network follows as a corollary rather than needing separate analysis.

• Distributed gates can beat teleportation in communication cost. The paper notes that applying a distributed two-qubit unitary (Section 8.1) requires only one bit of classical communication in each direction, rather than teleportation's two.

• The framework handles real protocols. Section 8 demonstrates applications including distributed control gates and the B92 quantum key distribution protocol.

• Not reported: the excerpt provides no performance measurements, benchmark timings, dataset sizes, or quantitative evaluation of the NetQASM pipeline; the claims are metatheoretic (proved) rather than empirical.

Methodology in Plain English

The authors build the system in layers. First, they take the quantum lambda calculus — a small functional language with linear types, where qubits have linear types and classical bits do not — and define its syntax, a small-step operational semantics over configurations consisting of an expression, a map from qubit references to positions in the quantum state, and a partial density matrix, plus a typing judgment splitting contexts into duplicable and linear parts. Partial density matrices are used so that measurement can be modeled nondeterministically rather than probabilistically. Second, they extend this to a choreographic language that adds actor-annotated local operations, classical message passing, and undirected entanglement generation. Third, they define a process language for individual nodes and an endpoint projection procedure that turns a choreography into a network of such processes. The central proof obligations — that well-typed programs do not get stuck, and that projection produces a network with the same semantics as the choreography — are discharged by induction over the typing and step relations, and every definition and theorem is checked by a proof assistant (Rocq) rather than on paper. Finally, they extract executable code from the Rocq development into NetQASM so that protocols can be simulated or run on network hardware.

Why This Matters

Impact on research. The paper opens a route for transferring decades of choreographic-programming results from classical distributed systems into quantum networking, and it supplies the first (per the authors) marriage of linear types with choreographies. Because the metatheory is mechanized, later work can build on a trustworthy foundation rather than re-verifying the core calculus.

Real-world applications.

• Quantum key distribution protocols such as B92, where correct ordering of quantum and classical messages is security-critical.
• Distributed quantum gates for scalable, modular quantum computers that link smaller processors via entanglement.
• Quantum teleportation and other state-transfer protocols across network links.
• Compilation of high-level network protocols down to hardware-controller instruction sets (NetQASM) for experimental quantum networks.

Industry relevance. Quantum networking hardware is moving from lab demonstrations toward programmable infrastructure; tooling that catches ordering and deadlock bugs at compile time rather than at runtime, and that targets an existing execution stack (NetQASM), is directly usable by groups building quantum network testbeds and by compiler teams who need a verified front end.

Future Directions

• Reported future work is not in the provided excerpt. Section 10 is described as concluding with comments on future work, but its contents are truncated here, so the authors' specific plans are not reported in the material above.
• Scaling the extraction pipeline. The paper demonstrates extraction to NetQASM but reports no quantitative evaluation; measuring overhead and validating against larger multi-node protocols is a natural next step.
• Richer network semantics. The current model assumes entanglement generation as the primitive quantum communication mechanism; incorporating noise, imperfect entanglement, and error correction would connect the calculus to realistic hardware.
• Broader protocol coverage and automation. Extending the language beyond the demonstrated examples (distributed control gates, B92) and integrating the Rocq-checked core into a practical compiler front end with tooling support.

Target Audience

Researchers and graduate students in quantum programming languages, programming-language theory, and formal verification; quantum network engineers and compiler developers who need correct-by-construction distributed protocols; and distributed-systems researchers already familiar with choreographies who want to see the paradigm extended to quantum communication.

Authors’ abstract

Programming distributed quantum systems requires multiple actors to coordinate precise sequences of quantum operations, classical communication, and entanglement generation. Writing such protocols directly as distributed processes is tedious and error-prone, and subtle mismatches can cause deadlock or silently incorrect quantum states. We present Qoreo, a choreographic programming language for quantum distributed systems in which an entire protocol is expressed as single, global program (a choreography) rather than as a collection of independent actor processes. Qoreo includes a local quantum language with linear types that enforce the no-cloning principle; a choreographic language that combines local quantum computation with inter-actor classical and quantum communication; and a process language for individual network nodes. We prove type safety for choreographies, guaranteeing that well-typed programs implement well-defined quantum operations, and we define endpoint projection~(EPP), which automatically derives a network of independent processes from any choreography. We prove EPP sound and complete with respect to the choreographic semantics; as a corollary, every well-typed choreography projects to a deadlock-free process network. The metatheory of Qoreo is fully mechanized in Rocq, and we provide an extraction pipeline to NetQASM for simulation and deployment on quantum network hardware.