面向代码安全性的量子中间表示形式化
量子物理
2023-03-28 v1 编程语言
摘要
量子中间表示（QIR）是微软开发的、基于 LLVM 的量子程序编译器中间表示。QIR 旨在为量子程序编译器提供独立于前端语言和后端硬件的通用解决方案，从而避免中间表示和编译器的重复开发。由于仍在开发中，QIR 以自然语言描述且缺乏形式化定义，导致其解释存在歧义且量子函数的实现缺乏严谨性。在本文中，我们为 QIR 的数据类型和指令集提供形式化定义，旨在为 QIR 中的操作和中间代码转换提供正确性与安全性保证。为验证我们的设计，我们展示了一些不安全的 QIR 代码示例，其中的错误可通过我们的形式化方法被检测出来。
引用
@article{arxiv.2303.14500,
title = {Formalization of Quantum Intermediate Representations for Code Safety},
author = {Junjie Luo and Jianjun Zhao},
journal= {arXiv preprint arXiv:2303.14500},
year = {2023}
}