Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qubit operations, it is mainly concerned with finding an assignment and inserting instructions to satisfy the connectivity constraints. Many methods have been proposed for the qubit allocation problem for low-level quantum programs. This paper presents a type-based framework of qubit allocation for a quantum programming language with first-order functions. In our framework, the connectivity constraints are expressed by a simple graph of qubits called a coupling graph. We formalize (1) the source language, whose type system verifies that the number of qubits required for a given program to run does not exceed the number of nodes of the coupling graph, (2) the target language, whose qualified type system verifies that a well-typed program satisfies the connectivity constraints, and (3) an algorithm to translate a source program into a target program. We prove that both languages are type-safe and that the translation algorithm is type preserving.

翻译：量子比特分配是将量子程序中的逻辑量子比特映射到物理量子比特的过程。由于某些量子计算机对双量子比特操作的应用存在连通性约束，该过程主要涉及寻找一种分配方案并插入指令以满足这些约束。针对低级量子程序的量子比特分配问题，已有多种方法被提出。本文提出了一种基于类型的框架，用于处理带有一阶函数的量子编程语言中的量子比特分配。在该框架中，连通性约束通过一个称为耦合图的简单量子比特图来表示。我们形式化了：(1) 源语言，其类型系统验证给定程序运行所需的量子比特数不超过耦合图的节点数；(2) 目标语言，其限定类型系统验证良类型程序满足连通性约束；(3) 将源程序翻译为目标程序的算法。我们证明这两种语言都是类型安全的，且翻译算法保持类型不变。