Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language

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.