Various physical constraints limit the number of qubits that can be implemented in a single quantum processor, and thus it is necessary to connect multiple quantum processors via quantum interconnects. While several compiler implementations for interconnected quantum computers have been proposed, there is no suitable representation as their compilation target. The lack of such representation impairs the reusability of compiled programs and makes it difficult to reason formally about the complicated behavior of distributed quantum programs. We propose InQuIR, an intermediate representation that can express communication and computation on distributed quantum systems. InQuIR has formal semantics that allows us to describe precisely the behaviors of distributed quantum programs. We give examples written in InQuIR to illustrate the problems arising in distributed programs, such as deadlock. We present a roadmap for static verification using type systems to deal with such a problem. We also provide software tools for InQuIR and evaluate the computational costs of quantum circuits under various conditions. Our tools are available at https://github.com/team-InQuIR/InQuIR.

翻译：各种物理约束限制了单台量子处理器中可实现的量子比特数量，因此需要通过量子互连将多台量子处理器连接起来。尽管已有多种针对互联量子计算机的编译器实现被提出，但目前尚缺乏合适的表示形式作为其编译目标。这种表示的缺失损害了编译程序的可重用性，并使得对分布式量子程序复杂行为的严格形式化推理变得困难。我们提出InQuIR，一种能够表达分布式量子系统上通信与计算的中间表示。InQuIR具有形式化语义，能够精确描述分布式量子程序的行为。我们通过InQuIR编写的示例说明了分布式程序中出现的典型问题（如死锁），提出了利用类型系统进行静态验证以解决此类问题的路线图，还提供了InQuIR的软件工具，并对不同条件下量子电路的计算开销进行了评估。我们的工具可通过 https://github.com/team-InQuIR/InQuIR 获取。