Author(s)

Takaaki Masuhara, Toru Kuriyama, Masakazu Yoshida^*, Jun Cheng

Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan.

Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are too big for humans to check the validity of them. The purpose of this work is to verify the validity of Robertson-type uncertainty relation toward verifying unconditional security of quantum key distributions. We verify the validity of the relation by using proof assistant Coq and it is turned out that the theorem regarding the relation formally holds. The source code for Coq which represents the validity of the theorem is printed in Appendix.

Formal Verification, Proof Assistant Coq, Uncertainty Relation

Masuhara, T. , Kuriyama, T. , Yoshida, M. and Cheng, J. (2015) Formal Verification of Robertson-Type Uncertainty Relation. Journal of Quantum Information Science, 5, 58-70. doi: 10.4236/jqis.2015.52008.