As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT) in which precise specifications about the modification to the quantum state can be provided within the type of a computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.

翻译：当量子计算机成为现实时,我们早就应该拿出有效的技术来帮助程序设计者编写正确的量子程序。在古典计算中的Hoare类型理论的启发下,我们提出了Qantum Hoare类型理论(QHTT),其中可以在计算类型中提供量子状态修改的确切规格。Hoare类型的这些规格以Hoare-log风格的预设和后期条件的形式,按照原样原则,以Hoare-logic风格的预设和后期形式给出。类型检查过程可以证实执行符合规定的规格。QHTT有可能成为量子程序的统一编程、具体说明和推理系统。