Towards a formally verified functional quantum programming language

Towards a formally verified functional quantum programming language
复制标题

迈向形式验证的函数式量子编程语言

DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. S. Green
A. S. Green
中科院分区：
--
文献类型：
--
作者：
A. S. Green

文献摘要

被引文献

相似文献

本论文着眼于开发一个函数量子编程语言的框架。该框架首先在Haskell中开发，研究如何使用一元结构来显式处理量子系统测量中固有的副作用，并继续研究Agda中的依赖类型重新实现如何为我们提供形式化的基础。 量子编程语言这两种实现本身并不是完全开发的量子编程语言，因为它们嵌入在各自的父语言中，但它们是朝着开发完全正式验证的功能性量子编程语言迈出的重要一步。被称为“量子IO Monad”，这个框架是按照量子计算的分类模型给出的结构方法设计的。
This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally verified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the “Quantum IO Monad”, this framework is designed following a structural approach as given by a categorical model of quantum computation.