机构名称：
¥ 1.0
随着量子计算机成为现实，我们是时候想出有效的技术来帮助程序员编写正确的量子程序了。在经典计算中，形式验证和健全的静态类型系统可以防止引入几类错误。在量子领域也需要类似的技术。受经典范式中霍尔类型理论 [NMB08] 的启发，我们提出了量子霍尔类型，通过扩展量子 IO Monad [AG09] 来提出量子霍尔类型，方法是使用前置条件和后置条件对其进行索引，作为程序规范。在本文中，我们介绍了量子霍尔类型理论 (QHTT)，介绍了它的语法和类型规则，并通过示例证明了它的有效性。QHTT 有可能成为一个用于编程、指定和推理量子程序的统一系统。这是一项正在进行的工作。1
量子霍尔类型理论
主要关键词
相关文件推荐
