As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.
翻译:当量子计算机成为现实时,我们早就应该拿出有效的技术来帮助程序设计者编写正确的量子程序。在古典计算中,正式的核查和声音静态类型系统防止了几种类型的错误被引入。在量子制度中需要类似的技术。在Hoare Type理论的启发下,我们建议了量子理论类型,通过用作为程序规格的预设和后设条件对量子理论进行索引来扩展量子理论的量子理论类型。在本文中,我们引入了 Quantum Hoare Type Theory (QHTT), 展示了它的语法和打字规则, 并以实例来展示其有效性。 QHTT有可能成为统一的量子程序编程系统, 具体描述和推理。 这是一项进展中的工作 。