Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language
Abstract
Given steady progress made in quantum technology research, the PI proposes to find new programming constructs and fragments of a new programming language that can support quantum computational algorithms and their verification. Quantum programming language is a fairly new research area that began to take its shape around 2005. In PI s recent work sponsored by IARPA, his team designed fragments of a quantum programming language, called Quipper, which was designed on top of Haskell for computing at the quantum circuit level. In this proposal, the PI proposes to expand his previous work to examine fundamental issues of a would-be quantum programming language: semantics; typing; quantum behaviors and effects; quantum data structures. The outcomes will be formalized and tested on proof assistants such as Coq and Agda.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 23, 2016
- Source ID
- FA95501510331
Entities
People
- Peter Selinger
Organizations
- Air Force Office of Scientific Research
- Dalhousie University
- United States Air Force