Search papers, labs, and topics across Lattice.
Qoreo introduces a choreographic programming language specifically designed for quantum distributed systems, allowing protocols to be expressed as a single global program rather than fragmented independent processes. This approach mitigates common issues such as deadlock and incorrect quantum states by enforcing type safety and ensuring that well-typed programs correspond to well-defined quantum operations. The framework includes a local quantum language with linear types and a mechanism for deriving independent processes from choreographies, validated through a fully mechanized metatheory in Rocq and an extraction pipeline to NetQASM for practical deployment.
Choreographic programming can eliminate deadlock and errors in quantum distributed systems by ensuring type safety and coherent protocol design.
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.
