一句话：为 QIR 的数据类型与指令集给出形式化定义，以保障量子中间代码操作与转换的正确性与安全性。
QIR 是微软基于 LLVM 为量子程序编译器提出的中间表示，旨在解耦前端语言与后端硬件。然而，当前 QIR 缺乏形式化定义，主要依赖自然语言描述，导致解释歧义，量子函数的实现也不够严谨。本文为 QIR 的数据类型和指令集建立形式化定义，从而为 QIR 内的操作以及中间代码转换提供正确性与安全性保证。作者通过构造不安全的 QIR 代码示例，展示该方法能够识别其中的错误，验证了形式化定义在提升 QIR 代码安全性方面的有效性。
Quantum Intermediate Representation (QIR) is an LLVM-based intermediate representation developed by Microsoft for quantum program compilers. QIR is designed to offer a universal solution for quantum program compilers, decoupled from both front-end languages and back-end hardware, thereby eliminating the need for redundant development of intermediate representations and compilers. However, the lack of a formal definition and reliance on natural language descriptions in the current state of QIR result in interpretational ambiguity and a dearth of rigor in implementing quantum functions. In this paper, we present formal definitions for QIR's data types and instruction sets to establish correctness and safety assurances for operations and intermediate code conversions within QIR. To demonstrate the effectiveness of our approach, we provide examples of unsafe QIR codes where errors can be identified with our method.