Skip to main content

Reasoning about, and stepwise development of, quantum programs: a predicate transformer semantics approach

Funding: 2010: $70,749
2011: $140,298
2012: $140,298
2013: $140,298
2014: $69,549

Project Member(s): Feng, Y.

Funding or Partner Organisation: Australian Research Council (ARC Future Fellowships)

Start year: 2011

Summary: The project will provide a framework to reason about, and stepwise develop, quantum programs by rigorous predicate transformer semantics, as well as breakthrough theory and frontier techniques for quantum software engineering. The outcomes will promote Australia's global research standing, and benefit industries and economies internationally.


Yu, N, Duan, R & Ying, M 2013, 'Five two-qubit gates are necessary for implementing the Toffoli gate', PHYSICAL REVIEW A, vol. 88, no. 1.
View/Download from: Publisher's site

Feng, Y, Yu, N & Ying, M 1970, 'Reachability Analysis of Recursive Quantum Markov Chains', MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013, International Symposium on Mathematical Foundations of Computer Science, Springer, IST Austria, pp. 385-396.
View/Download from: Publisher's site

Keywords: predicate transformer semantics, reasoning about quantum programs, refinement calculus, quantum programming language

FOR Codes: Computational Logic and Formal Languages, Quantum Information, Computation and Communication, Mathematical Aspects of Classical Mechanics, Quantum Mechanics and Quantum Information Theory, Expanding Knowledge in the Information and Computing Sciences, Information and Communication Services not elsewhere classified, Mathematical aspects of classical mechanics, quantum mechanics and quantum information theory, Quantum information, computation and communication, Other information and communication services not elsewhere classified