Article citationsMore>>

Gordon, M.J.C. (1986) Why Higher-Order Logic Is a Good Formalism for Specifying and Verifying Hardware. In: Milne, G.J. and Subrahmanyam, P.A., Eds., Proceedings of the 1985 Edinburgh Workshop on VLSI, North-Holland, 153-177.

has been cited by the following article:

• TITLE: Formal Verification of Robertson-Type Uncertainty Relation

  AUTHORS: Takaaki Masuhara, Toru Kuriyama, Masakazu Yoshida, Jun Cheng

  KEYWORDS: Formal Verification, Proof Assistant Coq, Uncertainty Relation

  JOURNAL NAME: Journal of Quantum Information Science, Vol.5 No.2, June 11, 2015

  ABSTRACT: 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.