Qoreo: Choreographic Programming for Quantum Distributed Systems

Qoreo introduces a choreographic programming language for quantum distributed systems, where an entire protocol is expressed as a single global program rather than separate actor processes. The method combines a local quantum language with linear types to enforce the no-cloning principle, a choreographic language for inter-actor communication, and a process language for network nodes. The authors prove type safety and define endpoint projection (EPP), which automatically derives a deadlock-free network of independent processes from any choreography, with the metatheory fully mechanized in Rocq. This matters because it eliminates tedious and error-prone manual coordination, ensuring correct quantum operations and deadlock-free execution for distributed quantum systems.