Coupling Techniques for Reasoning about Quantum Programs

量子软件对于释放量子计算的超级能力是不可或缺的。该项目旨在首次开发用于推理量子程序等价性的有效技术，并应用于验证量子编译器和量子密码协议。该项目中提出的成果和工具的成功开发将大大推进量子编程理论的逻辑和数学基础知识，从而帮助澳大利亚行业建立量子软件工程的前沿技术-特别是量子编译器-以及建立和保持其在量子计算时代的竞争地位。

Quantum software is indispensable for unleashing the super-power of quantum computing. This project aims to develop, for the first time, effective techniques for reasoning about the equivalence of quantum programs, with applications for verifying quantum compilers and quantum cryptographic protocols. The successful development of the outcomes and tools proposed in this project will significantly advance the knowledge on logical and mathematical foundations of quantum programming theory and thereby help Australian industries to build frontier technologies for quantum software engineering – in particular for quantum compilers – as well as establish and preserve their competitive status in the quantum computing era.