Pith. sign in

REVIEW 2 major objections 5 minor 35 references

This paper introduces Qoreo, a choreographic programming language for distributed quantum systems, and proves that every well-typed choreography projects to a deadlock-free process network.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 09:58 UTC pith:3GPCC5AK

load-bearing objection Strong formal PL/quantum paper with a genuinely important idea, but the displayed typing rules appear to admit self-send choreographies, which would sink the deadlock-freedom corollary; the fix is likely a missing A≠B side condition, and the preprint must state it. the 2 major comments →

arxiv 2607.20391 v1 pith:3GPCC5AK submitted 2026-07-22 quant-ph cs.PL

Qoreo: Choreographic Programming for Quantum Distributed Systems

Jennifer Paykin , Steven Baldasty , Joseph P. Near , Christian Skalka This is my paper
classification quant-ph cs.PL MSC 68N1568Q8581P68
keywords choreographic programmingdistributed quantum systemsendpoint projectionlinear typesdeadlock freedomentanglement generationquantum teleportationtype safety
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper argues that distributed quantum protocols can be written as a single global program—a choreography—rather than as separate, manually synchronized actor processes, and that this style is both practical and safe. It introduces Qoreo, with a linear type system that forbids cloning or discarding qubits, and endpoint projection (EPP) that automatically extracts each actor's process from the choreography. The main theorem is that projection preserves semantics in both directions (soundness and completeness), and as a corollary every well-typed choreography yields a deadlock-free process network. If this holds, quantum protocol programmers can reason about the whole protocol in one place and obtain correct, deadlock-free distributed implementations without writing or debugging per-node processes. The metatheory is fully mechanized in a proof assistant, and an extraction pipeline to a real quantum network instruction set is provided.

Core claim

Qoreo's central discovery is that choreographic programming can be carried into the quantum setting without giving up the guarantees that matter: type safety for the global program, and deadlock freedom plus semantic preservation for the projected network. The key is a linearly typed choreographic language in which each qubit is owned by exactly one actor, cannot be duplicated or discarded, and can be transmitted only via entanglement generation, combined with an endpoint projection that filters a choreography into per-actor send, receive, entangle, and local-computation processes. Theorems 6.2 and 6.5 show that EPP is sound and complete: every choreographic step is matched by the projected

What carries the argument

Endpoint projection (EPP), the filtering operation that turns a global choreography into a network of one process per actor, is the central mechanism. It is supported by a linear type system that tracks qubit ownership and forbids cloning, and by a 'delay' rule in the choreographic semantics that allows independent actor steps to be interleaved. EPP is the bridge that makes deadlock freedom by construction: a deadlock would be a stuck choreographic configuration, which type safety rules out, and EPP soundness/completeness ensures the projected network inherits exactly the choreography's step behavior.

Load-bearing premise

The deadlock-freedom and semantic-preservation theorems assume an idealized network where entanglement generation is atomic and lossless, communication is synchronous, and the whole system shares one global quantum state; real asynchronous, lossy, or buffered hardware is outside the proof.

What would settle it

Run the extracted processes on an asynchronous or lossy quantum network simulator: if a well-typed Qoreo choreography's projected processes can deadlock or diverge from the choreographic semantics under those conditions, the paper's corollary does not transfer to such hardware. Within the paper's own model, a counterexample would be a well-typed choreography whose projected network reaches a non-terminal state with no enabled step—something the proof says cannot occur.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Programmers can express protocols such as quantum teleportation, distributed controlled gates, and quantum key distribution as single global programs and automatically obtain correct local processes.
  • Well-typed Qoreo programs cannot deadlock or clone qubits, because such failures would contradict Corollary 6.6 or the linear type safety theorems.
  • EPP soundness and completeness mean that reasoning about the global choreography, including the evolution of the shared quantum state, transfers to the asynchronous network of processes.
  • The proof-assistant mechanization gives machine-checked assurance for the metatheory, and the extraction pipeline maps verified choreographies to runnable code for simulators and hardware.
  • Since well-typed choreographies are guaranteed projectable, the language avoids the common process-level errors of forgotten or reordered messages that cause deadlock or silently corrupted quantum states.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The global-view style makes Qoreo a natural target for resource analysis: one could compute communication depth or Bell-state usage over the choreography, then apply optimizations that are difficult to state process-by-process; this direction is left implicit in the paper.
  • If later extended with knowledge of choice, a Qoreo-like language could handle protocols with dynamically determined communication patterns; the authors note this as future work without developing it.
  • Treating each entangled pair as a linear resource would extend the same typing discipline to explicit resource accounting, an analogy the paper does not pursue.
  • A stress test on real asynchronous, lossy hardware—where entanglement attempts can fail—would reveal which parts of the deadlock-freedom result depend on the idealized entanglement primitive, even though such realism is explicitly outside the paper's theorems.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces Qoreo, a choreographic programming language for distributed quantum systems. A programmer writes a global choreography combining local quantum computations, classical message passing, and entanglement generation; endpoint projection (EPP) automatically derives a process network. The paper presents a local quantum lambda calculus with linear types, a choreographic language, a process language, and proves type safety for choreographies, EPP soundness and completeness, and a deadlock-freedom corollary for projected networks. The metatheory is mechanized in Rocq, and an extraction pipeline to NetQASM is described. Examples include quantum teleportation, distributed controlled gates, and B92 quantum key distribution.

Significance. If the claims hold, this is a substantial contribution: it is the first system, to my knowledge, to combine linear types with choreographic programming for distributed quantum protocols, and it provides machine-checked proofs of the key metatheoretic results. The paper explicitly names Rocq lemmas for the load-bearing theorems, and the semantic rules and typing rules are presented in enough detail that the intended proof architecture is visible. The extraction pipeline to NetQASM, though not verified end-to-end, is a useful practical step. The main concern, detailed below, is a missing side condition in the displayed typing rules that is load-bearing for the central deadlock-freedom corollary.

major comments (2)
  1. [§6.1, Fig. 8, Corollary 6.6] The displayed send and entangle typing rules contain no A ≠ B side condition. As written, the choreography A.!true ⇝ A.x; 0 is typeable: the continuation 0 has only the classical binding A.x, so no linear variables remain, and the empty choreography is typeable according to §7. Its endpoint projection is A[send !true to A; 0], which is stuck because the network communication rule com-C requires A ≠ B. Similarly, A.x ↭ A.y; 0 is typeable under the entangle rule and projects to a self-entanglement that cannot reduce under com-Q. This directly falsifies Lemma 6.1(1) and hence Corollary 6.6 for the system as presented. If the Rocq formalization includes A ≠ B side conditions in these rules, the manuscript must display them and state that they are part of the typing judgment; otherwise the proof of Lemma 6.1(1) cannot be checked from the preprint. This is the exact point at which well-typedne
  2. [Fig. 8, entangle rule] The entangle rule has the same omission as the send rule: it allows A.x ↭ B.y with A = B. Since the paper defines 'well-formed' to exclude self-communication, and Lemma 6.1(1) asserts that typing enforces well-formedness, the entangle rule needs an explicit A ≠ B side condition (or the definition of well-formedness must be extended to cover self-entanglement). The current presentation leaves a second route to the counterexample described above.
minor comments (5)
  1. [§7, Lemma 7.1] Typo: 'tleeport' should be 'teleport'.
  2. [§4.1] The labels paragraph says 'a classical communication between A and B (written A↭B)'; this should be 'quantum communication' or 'entanglement generation'.
  3. [Lemma 4.7] The statement contains a malformed configuration '⟨𝐶′;Θ;′⟩𝜌′'; it should read '⟨𝐶′; Θ′; 𝜌′⟩'.
  4. [§3.1 and §4.1] 'Reflective transitive closure' should be 'reflexive transitive closure'.
  5. [§10.3 and §6] The paper appropriately scopes out noise and dynamic actors, but the abstract's deadlock-freedom claim should be explicitly qualified as relative to the idealized atomic, lossless, synchronous network model; a sentence in the abstract or introduction would prevent over-reading.

Circularity Check

0 steps flagged

No circularity: deadlock-freedom is derived from proved type safety, EPP soundness/completeness, and the Rocq mechanization—not from fitted inputs or load-bearing self-citations.

full rationale

Qoreo's main derivation chain is self-contained rather than circular. Local type safety is proved in Theorem 3.8, choreographic type safety in Theorem 4.8, and EPP soundness/completeness in Theorems 6.2 and 6.5; Corollary 6.6 is a direct composition of those results. The network language has its own independent operational semantics in Fig. 9, and the soundness/completeness theorems prove a lockstep correspondence between choreographic and network behavior rather than defining the result into existence. There are no fitted parameters, no data-dependent predictions, no imported uniqueness theorem, and no load-bearing self-citations; the claim that the metatheory is fully mechanized in Rocq is external evidence of the derivation's existence. Two manuscript-internal concerns are worth flagging but are not circularity: (i) the typing rules in Fig. 8 omit an explicit A≠B side condition even though Lemma 6.1(1) asserts that typing enforces well-formedness, so a self-send (or self-entangle) choreography may be typeable and project to a stuck network—this is a soundness gap in the written argument, not a reduction of a prediction to its inputs; and (ii) Section 10 explicitly scopes out noise, decoherence, and dynamic actors, so the theorems cover only the idealized atomic-entanglement, synchronous model—again a scope limitation, not a circular step. Under the hard rule that circularity requires demonstrating a specific reduction of a result to its own inputs, the appropriate score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

This is a formal language/metatheory paper, so the ledger records modeling assumptions rather than fitted parameters. There are no fitted constants or hand-tuned coefficients; the central guarantees are conditional on the global-density-matrix and ideal-synchronous-entanglement model.

axioms (5)
  • domain assumption Quantum system state is a single global partial density matrix; qubit references map to indices in this matrix.
    Used throughout Sections 3.1 and 4.1; this abstracts away per-node memory and asynchronous local state.
  • domain assumption Entanglement generation is an atomic, lossless primitive that produces the Bell state |Φ+>.
    entangleB (Fig. 7) and com-Q (Fig. 9); no routing, failure, or decoherence is modeled, so all deadlock/state guarantees are relative to this ideal.
  • domain assumption Classical and quantum communication are synchronous; send/receive and entangle actions must match exactly.
    Network step rules com-C and com-Q (Fig. 9); EPP soundness/completeness assume this synchronization.
  • ad hoc to paper The actor set is fixed and known at projection time; conditional choreographies are omitted.
    Section 4 syntax has no conditionals; Sections 9 and 10 note dynamic participation and knowledge of choice as future work. This restricts the class of protocols covered.
  • standard math The Rocq proof assistant and the submitted repository are correct and match the paper's definitions.
    All metatheorems are claimed mechanized; without inspecting the artifact with a pinned commit, this trust assumption remains unverified.

pith-pipeline@v1.3.0-alltime-deepseek · 22737 in / 23716 out tokens · 205568 ms · 2026-08-01T09:58:14.961924+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2607.20391 by Christian Skalka, Jennifer Paykin, Joseph P. Near, Steven Baldasty.

Figure 1
Figure 1. Figure 1: Quantum teleportation protocol as an informal quantum circuit diagram. Alice starts with an arbitrary [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Implementation of the quantum teleportation protocol in the quantum process model. The syntax [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Quantum teleportation as a choreography. On [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Qoreo syntax Definition 3.1. Let 𝑀1, 𝑀2 be finite maps with keys 𝑘. We write 𝑀1, 𝑀2 to mean the concatenation of the two maps, e.g. 𝑀 such that 𝑀(𝑘) = 𝑀2 (𝑘) if 𝑘 ∈ dom(𝑀2), otherwise 𝑀(𝑘) = 𝑀1 (𝑘). We write 𝑀1⊥𝑀2 to mean dom(𝑀1) ∩ dom(𝑀2) = ∅. 3.1 Operational semantics We define a small-step call-by-value operational semantics on configurations of the form ⟨𝑒; Θ; 𝜌⟩, where 𝑒 is a closed expression, 𝜌 is a… view at source ↗
Figure 5
Figure 5. Figure 5: Step relation rules for the local quantum language. The first group consists of contextual reduction rules [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Typing rules for the local quantum language. Above the line are rules for the linear lambda calculus, [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Select operational semantics for choreographies. In the [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Select typing rules for the choreographic language. [PITH_FULL_IMAGE:figures/full_fig_p012_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Operational semantics rules for networks. Substitution in processes [PITH_FULL_IMAGE:figures/full_fig_p014_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Rocq data structures representing Qoreo ASTs. We use the OCaml/Rocq convention of defining [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Extraction pipeline from a global Qoreo choreography to simulation using NetQASM. [PITH_FULL_IMAGE:figures/full_fig_p017_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Distributed protocol for implementing a 2-qubit controlled-unitary [ [PITH_FULL_IMAGE:figures/full_fig_p018_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: An implementation of an 𝑛-controlled gate distributed across 𝑛 actors. The function distributed_n_CU takes as input a list of actors 𝐴 with qubit variables 𝑞𝑠, and a single target actor 𝐵 with qubit 𝑡𝑔𝑡. The goal of the protocol is to apply the input controlled unitary 𝐶𝑈 to the controls 𝑞𝑠 and target 𝑡𝑔𝑡. The helper functions fmap and fmap2 fold over the input lists and concatenate the results together, … view at source ↗
Figure 14
Figure 14. Figure 14: B92 Algorithm 8.2 Quantum Key Distribution / B92 In quantum key distribution (QKD), two parties (Alice and Bob) establish a secret key using a quantum channel and a classical channel. The quantum channel is insecure: an eavesdropper (Eve) may measure, resend, or otherwise manipulate the entangled pairs it generates. The classical channel is authenticated but not confidential: Eve may read the messages tha… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 3 canonical work pages

  1. [1]

    Economou, David Elkouss, Paul Hilaire, Liang Jiang, Hoi-Kwong Lo, and Ilan Tzitrin

    Koji Azuma, Sophia E. Economou, David Elkouss, Paul Hilaire, Liang Jiang, Hoi-Kwong Lo, and Ilan Tzitrin. 2023. Quantum repeaters: From quantum networks to the quantum internet.Reviews of Modern Physics95, 4 (Dec. 2023), 045006. doi:10.1103/RevModPhys.95.045006

    doi:10.1103/revmodphys.95.045006 2023

  2. [2]

    Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, and Patrick Eugster. 2024. An Algebraic Language for Specifying Quantum Networks.Artifact for the article An Algebraic Language for Specifying Quantum Networks8, PLDI (June 2024), 200:1313–200:1335. doi:10.1145/3656430 , Vol. 1, No. 1, Article . Publication date: July 2026. 22 Jenni...

    work page doi:10.1145/3656430 2024

  3. [3]

    Luís Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. InInternational Conference on Concurrency Theory. Springer, 222–236

    2010

  4. [4]

    Marcello Caleffi, Michele Amoretti, Davide Ferrari, Jessica Illiano, Antonio Manzalini, and Angela Sara Cacciapuoti

  5. [5]

    Yuan Cao, Yongli Zhao, Qin Wang, Jie Zhang, Soon Xin Ng, and Lajos Hanzo. 2022. The Evolution of Quantum Key Distribution Networks: On the Road to the Qinternet.IEEE Communications Surveys & Tutorials24, 2 (2022), 839–894. doi:10.1109/COMST.2022.3144219

    arXiv 2022

  6. [6]

    Marco Carbone, Luís Cruz-Filipe, Fabrizio Montesi, and Agata Murawska. 2018. Multiparty classical choreographies. InInternational Symposium on Logic-Based Program Synthesis and Transformation. Springer, 59–76

    2018

  7. [7]

    Marco Carbone and Fabrizio Montesi. 2013. Deadlock-freedom-by-design: multiparty asynchronous global program- ming.ACM SIGPLAN Notices48, 1 (2013), 263–274

    2013

  8. [8]

    Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. 2018. Choreographies, logically.Distributed Computing31, 1 (Feb. 2018), 51–67. doi:10.1007/s00446-017-0295-1

    work page doi:10.1007/s00446-017-0295-1 2018

  9. [9]

    Javier Cardama and Tomás F

    F. Javier Cardama and Tomás F. Pena. 2025. NetQMPI: a practical MPI-inspired library for distributed quantum computing over NetQASM SDK. In2025 IEEE International Conference on Cluster Computing Workshops (CLUSTER Workshops). 1–2. doi:10.1109/CLUSTERWorkshops65972.2025.11164201

    arXiv 2025

  10. [10]

    Tim Coopmans, Robert Knegjens, Axel Dahlberg, David Maier, Loek Nijsten, Julio de Oliveira Filho, Martijn Papendrecht, Julian Rabbie, Filip Rozpędek, Matthew Skrzypczyk, Leon Wubben, Walter de Jong, Damian Podareanu, Ariana Torres- Knoop, David Elkouss, and Stephanie Wehner. 2021. NetSquid, a NETwork Simulator for QUantum Information using Discrete events...

    doi:10.1038/s42005-021-00647-8 2021

  11. [11]

    Luís Cruz-Filipe and Fabrizio Montesi. 2017. Procedural Choreographic Programming. 92–107 pages

    2017

  12. [12]

    Axel Dahlberg, Bart van der Vecht, Carlo Delle Donne, Matthew Skrzypczyk, Ingmar te Raa, Wojciech Kozlowski, and Stephanie Wehner. 2022. NetQASM – A low-level instruction set architecture for hybrid quantum-classical programs in a quantum internet.Quantum Science and Technology7, 3 (July 2022), 035023. doi:10.1088/2058-9565/ac753f arXiv:2111.09823 [quant-ph]

    Pith/arXiv arXiv 2022

  13. [13]

    Axel Dahlberg and Stephanie Wehner. 2017. SimulaQron – A simulator for developing quantum internet software. arXiv:1712.08032 [quant-ph]

    Pith/arXiv arXiv 2017

  14. [14]

    Timothy AS Davidson, Simon J Gay, Hynek Mlnarik, Rajagopal Nagarajan, and Nick Papanikolaou. 2012. Model Checking for Communicating Quantum Processes.Int. J. Unconv. Comput.8, 1 (2012), 73–98

    2012

  15. [15]

    Stephen DiAdamo, Janis Nötzel, Benjamin Zanger, and Mehmet Mert Beşe. 2020. QuNetSim: A Software Framework for Quantum Networks. arXiv:2003.06397 [quant-ph]

    Pith/arXiv arXiv 2020

  16. [16]

    Simon J Gay and Rajagopal Nagarajan. 2005. Communicating quantum processes. InProceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages. 145–157

    2005

  17. [17]

    Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2024. Choral: Object-oriented Choreographic Programming. ACM Trans. Program. Lang. Syst.46, 1 (Jan. 2024), 1:1–1:59. doi:10.1145/3632398

    doi:10.1145/3632398 2024

  18. [18]

    Green, Peter LeFanu Lumsdaine, Neil J

    Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum programming language. InProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’13). Association for Computing Machinery, New York, NY, USA, 333–342. doi:10.1145/2491956.2462177

    arXiv 2013

  19. [19]

    Andrew K Hirsch and Deepak Garg. 2022. Pirouette: higher-order typed functional choreographies.Proceedings of the ACM on Programming Languages6, POPL (2022), 1–27

    2022

  20. [20]

    Vasconcelos, and Makoto Kubo

    Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. InEuropean Symposium on Programming (ESOP). Springer, 122–138

    1998

  21. [21]

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. InProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 273–284

    2008

  22. [22]

    Mark Koch, Agustín Borgna, Craig Roy, Alan Lawrence, Kartik Singhal, Seyon Sivarajah, and Ross Duncan. 2025. Imperative Quantum Programming with Ownership and Borrowing in Guppy. doi:10.48550/arXiv.2510.13082

    doi:10.48550/arxiv.2510.13082 2025

  23. [23]

    Wojciech Kozlowski, Axel Dahlberg, and Stephanie Wehner. 2020. Designing a quantum network protocol. In Proceedings of the 16th International Conference on emerging Networking EXperiments and Technologies (CoNEXT ’20). Association for Computing Machinery, New York, NY, USA, 1–16. doi:10.1145/3386367.3431293

    arXiv 2020

  24. [24]

    Ivan Lanese, Ugo Dal Lago, and Vikraman Choudhury. 2025. Towards Quantum Multiparty Session Types. InSoftware Engineering and Formal Methods, Alexandre Madeira and Alexander Knapp (Eds.). Springer Nature Switzerland, Cham, 385–403. doi:10.1007/978-3-031-77382-2_22

    doi:10.1007/978-3-031-77382-2_22 2025

  25. [25]

    2023.Introduction to Choreographies

    Fabrizio Montesi. 2023.Introduction to Choreographies. Cambridge University Press

    2023

  26. [26]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. doi:10.1017/CBO9780511976667 , Vol. 1, No. 1, Article . Publication date: July 2026. Qoreo: Choreographic Programming for Quantum Distributed Systems 23

    doi:10.1017/cbo9780511976667 2010

  27. [27]

    Moein Sarvaghad-Moghaddam and Mariam Zomorodi. 2021. A general protocol for distributed quantum gates. Quantum Information Processing20, 8 (2021), 265

    2021

  28. [28]

    Peter Selinger. 2004. Towards a quantum programming language.Mathematical Structures in Computer Science14, 4 (Aug. 2004), 527–586. doi:10.1017/S0960129504004256

    doi:10.1017/s0960129504004256 2004

  29. [29]

    Peter Selinger and Benoît Valiron. 2009. Quantum Lambda Calculus. InSemantic Techniques in Quantum Computation (1 ed.), Simon Gay and Ian Mackie (Eds.). Cambridge University Press, 135–172. doi:10.1017/CBO9781139193313.005

    work page doi:10.1017/cbo9781139193313.005 2009

  30. [30]

    Gan Shen, Shun Kashiwa, and Lindsey Kuper. 2023. HasChor: Functional Choreographic Programming for All (Functional Pearl).Proc. ACM Program. Lang.7, ICFP, Article 207 (Aug. 2023), 25 pages. doi:10.1145/3607849

    doi:10.1145/3607849 2023

  31. [31]

    Stephanie Wehner, David Elkouss, and Ronald Hanson. 2018. Quantum internet: A vision for the road ahead.Science 362, 6412 (2018). doi:10.1126/science.aam9288

    doi:10.1126/science.aam9288 2018

  32. [32]

    Xiaoliang Wu, Alexander Kolar, Joaquin Chung, Dong Jin, Tian Zhong, Rajkumar Kettimuthu, and Martin Suchara

  33. [33]

    Yun Zheng, Hanyu Wang, Xinyu Jia, Jiahui Huang, Huihong Yuan, Chonghao Zhai, Junhao Dai, Jingbo Shi, Lei Zhang, Xuguang Zhang, Minxue Zhuang, Jinchang Liu, Jun Mao, Tianxiang Dai, Zhaorong Fu, Yuqing Jiao, Yaocheng Shi, Daoxin Dai, Xingjun Wang, Yan Li, Qihuang Gong, Zhiliang Yuan, Lin Chang, and Jianwei Wang. 2026. Large-scale quantum communication netwo...

    2026

  34. [2020]

    arXiv:2009.12000 [quant-ph]

    SeQUeNCe: A Customizable Discrete-Event Simulator of Quantum Networks. arXiv:2009.12000 [quant-ph]

    Pith/arXiv arXiv 2009

  35. [2024]

    2024), 110672

    Distributed quantum computing: A survey.Computer Networks254 (Dec. 2024), 110672. doi:10.1016/j.comnet. 2024.110672

    arXiv 2024