Formal Meta-level Analysis Framework for Quantum Programming Languages
Mohamed Yousri Mahmoud, Amy Felty · 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.