Formal Meta-level Analysis Framework for Quantum Programming Languages.
Electronic Notes in Theoretical Computer Science(2018)
摘要
The design and development of quantum programming languages (QPLs) is an important and active area of quantum computing. This paper addresses the problem of developing a standard methodology for verifying a QPL against major quantum computing concepts. We propose a framework dedicated to the meta-level analysis of QPLs, in particular, functional quantum languages. To this aim, we choose the Hybrid system as the tool in which to build our framework. Hybrid is a logical framework that supports higher-order abstract syntax, on top of which we develop an intuitionistic linear specification logic used for reasoning about QPLs. We provide a formal proof of some important meta-theoretic properties of this logic, and in addition, showcase a number of examples that can be tackled under the proposed framework.
更多查看译文
关键词
Quantum Lambda Calculus,Linear Logic,Hybrid,Coq
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要