Mingsheng Ying
Abstract
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
- Akatov, D. 2005. The logic of quantum program verification. M.S. thesis, Oxford University Computing Laboratory.Google Scholar
- Altenkirch, T. and Grattage, J. 2005. A functional quantum programming language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05). 249--258. Google ScholarDigital Library
- Apt, K. R. and Olderog, E. R. 1997. Verification of Sequential and Concurrent Programs. Springer, Berlin. Google ScholarDigital Library
- Baltag, A. and Smets, S. 2004. The logic of quantum programs. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04).Google Scholar
- Baltag, A. and Smets, S. 2006. Lqp: The dynamic logic of quantum information. Math. Structures Comput. Sci. 16, 491--525. Google ScholarDigital Library
- Bettelli, S., Calarco, T., and Serafini, L. 2003. Toward an architecture for quantum programming. Euro. Phys. J. D 25, 181--200.Google Scholar
- Birkhoff, G. and Von Neumann, J. 1936. The logic of quantum mechanics. Ann. Math. 37, 823--843.Google ScholarCross Ref
- Brunet, O. and Jorrand, P. 2004. Dynamic quantum logic for quantum programs. Int. J. Quantum Inf. 2, 45--54.Google ScholarCross Ref
- Chadha, R., Mateus, P., and Sernadas, A. 2006. Reasoning about imperative quantum programs. Electron. Notes Theor. Comput. Sci. 158, 19--39. Google ScholarDigital Library
- D'Hondt, E. and Panangaden, P. 2006. Quantum weakest preconditions. Math. Structures Comput. Sci. 16, 429--451. Google ScholarDigital Library
- Feng, Y., Duan, R. Y., Ji, Z. F., and Ying, M. S. 2007. Proof rules for the correctness of quantum programs. Theor. Comput. Sci. 386, 151--166. Google ScholarDigital Library
- Feng, Y., Duan, R. Y., and Ying, M. S. 2011. Bisimulation for quantum processes. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11). ACM, New York, 523--534. Google ScholarDigital Library
- Gay, S. J. 2006. Quantum programming languages: survey and bibliography. Math. Structures Comput. Sci. 16, 581--600. Google ScholarDigital Library
- Gay, S. J. and Nagarajan, R. 2005. Communicating quantum processes. In Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'05). ACM, New York, 145--157. Google ScholarDigital Library
- Grover, L. 1996. A fast quantum mechanical algorithm for database searches. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing. ACM, New York, 212--219. Google ScholarDigital Library
- Jorrand, P. and Lalire, M. 2005. Toward a quantum process algebra. In Proceedings of the First ACM Conference on Computing Frontiers. ACM, New York, 111--119. Google ScholarDigital Library
- Knill, E. H. 1996. Conventions for quantum pseudocode. Tech. rep. LAUR-96-2724, Los Alamos National Laboratory.Google Scholar
- Morgan, C. 1995. Proof rules for probabilistic loops. Tech. rep. PRG-TR-25-95, Programming Research Group, Oxford University.Google Scholar
- Nielsen, I. L. and Chuang, M. A. 2000. Quantum Computation and Quantum Information. Cambridge University Press, Cambridge, UK. Google ScholarDigital Library
- Ömer, B. 2003. Structural quantum programming. Ph.D. dissertation, Technical University of Vienna.Google Scholar
- Sanders, J. W. and Zuliani, P. 2000. Quantum programming. In Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 1837. Springer, Berlin, 88--99. Google ScholarDigital Library
- Selinger, P. 2004a. A brief survey of quantum programming languages. In Proceedings of the 7th International Symposium on Functional and Logic Programming. Lecture Notes in Computer Science, vol. 2998, Springer, Berlin.Google Scholar
- Selinger, P. 2004b. Towards a quantum programming language. Math. Structures Comput. Sci. 14, 527--586. Google ScholarDigital Library
- Von Neumann, J. 1938. On infinite direct products. Compos. Math. 6, 1--77.Google Scholar
- Ying, M. S., Duan, R. Y., Feng, Y., and Ji, Z. F. 2010. Predicate Transformer Semantics of Quantum Programs. Cambridge University Press, 311--360.Google Scholar
- Ying, M. S., Feng, Y., Duan, R. Y., and Ji, Z. F. 2009. An algebra of quantum processes. ACM Trans. Comput. Logic 10, 19, 1. Google ScholarDigital Library
- Zuliani, P. 2004. Nondeterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04).Google Scholar
Index Terms
- Floyd--hoare logic for quantum programs
Recommendations
An applied quantum Hoare logic
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: 1. restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of ...
A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs
Essays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 9660A simple dynamically-typed, purely object-oriented language is defined. A structural operational semantics as well as a Hoare-style program logic for reasoning about programs in the language in multiple notions of correctness are given. The Hoare logic ...
Formalization of the Resolution Calculus for First-Order Logic
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
Comments