[Under construction]2015 AFOSR MURISemantics, Formal Reasoning, and Tool Support for Quantum ProgrammingPO: Dr. Tristan Nguyen, Information Assurance and CybersecurityPI: Dr. Michael Mislove, Tulane UniversityWebsite: TBD
Research Problem and Technical Approaches: The looming appearance of universal quantum computers makes it is imperative to devise methods for correctly programming such devices. Quantum algorithms are complex, and quantum computers explore alternative computation branches in superposition, so programming mistakes in even minor parts of the code can alter the quantum state and invalidate the final result. Debugging is inappropriate in the quantum setting, since it requires examining the program state, and besides the high cost of early quantum computers will make trial runs prohibitively expensive. The goal of this project is to devise novel methods for ensuring quantum programs are correct. We will use emerging alternative models for quantum computing that we are developing to devise methods to reason effectively about quantum computations, and we test our methods on the functional quantum programming language Quipper.
Our approach is based on Formal Verification, an approach that ensures programs are correct before implementation and that can be carried out in advance of having quantum computers. We will use our mathematical models to devise the tools and methods we need to formally analyze quantum programming and quantum computing. Our methodology will be tested on a formalized version of Quipper, using a mathematical semantics we will develop, together with methods and tools tailored to reason about quantum programs. Our research will produce a simple yet expressive methodology for analyzing quantum computing and functional quantum programming languages.
Anticipated Outcomes: We anticipate novel models and toolsets specifically designed for analyzing quantum programs, together with methods for their effective use. These will be based on advances in modeling quantum mechanics that we will devise. The result will be a better understanding of the potential of quantum computation and of the relation between quantum and classical computing, as well as deep insights into the potential gains and threats quantum computers pose for the security infrastructure, and into their potential uses for application in materials simulation and related areas that strain the current limits of high performance computing.
Impact on DoD Capabilities: This project will provide a better understanding of the power of quantum computing and of the threats that it poses. DOD relies on network communications, and the security of its systems could be compromised by quantum computing. This research will help clarify the extent of such a threat. Quantum computing promises revolutionary increases in computing power that can be applied to important areas such as materials design and analysis, machine learning, protein folding, climate simulation, and similar areas that require high performance computing. Realizing the advances anticipated in quantum computing requires correct programs, which is the theme of this project.