양자 분산 시스템 (distributed quantum systems)을 프로그래밍하려면 여러 액터 (actors)가 양자 연산 (quantum operations), 고전적 통신 (classical communication), 그리고 얽힘 생성 (entanglement generation)의 정밀한 시퀀스를 조정해야 합니다. 이러한 프로토콜을 분산 프로세스로 직접 작성하는 것은 지루하고 오류가 발생하기 쉬우며, 미세한 불일치는 데드락 (deadlock)을 유발하거나 조용히 잘못된 양자 상태를 초래할 수 있습니다. 우리는 전체 프로토콜을 독립적인 액터 프로세스들의 집합이 아닌, 단일한 전역 프로그램 (choreography, 안무)으로 표현하는 양자 분산 시스템을 위한 안무 프로그래밍 언어 (choreographic programming language)인 Qoreo를 제시합니다. Qoreo는 복제 불가능 원리 (no-cloning principle)를 강제하는 선형 타입 (linear types)을 포함한 로컬 양자 언어 (local quantum language), 로컬 양자 연산과 액터 간의 고전적 및 양자 통신을 결합하는 안무 언어 (choreographic language), 그리고 개별 네트워크 노드를 위한 프로세스 언어 (process language)를 포함합니다. 우리는 안무 (choreographies)에 대한 타입 안전성 (type safety)을 증명하여, 잘 정의된 타입의 프로그램이 잘 정의된 양자 연산을 구현함을 보장하며, 임의의 안무로부터 독립적인 프로세스 네트워크를 자동으로 도출하는 엔드포인트 투영 (endpoint projection, EPP)을 정의합니다. 우리는 EPP가 안무 의미론 (choreographic semantics)에 대해 건전성 (sound)과 완전성 (complete)을 가짐을 증명하며, 그 결과로 모든 잘 정의된 타입의 안무는 데드락이 없는 프로세스 네트워크로 투영됩니다. Qoreo의 메타 이론 (metatheory)은 Rocq에서 완전히 기계화되었으며, 시뮬레이션 및 양자 네트워크 하드웨어 배포를 위해 NetQASM으로의 추출 파이프라인 (extraction pipeline)을 제공합니다.