Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Verification of quantum protocols using Coq

Jaap Boender, Florian Kammueller, Rajagopal Nagarajan

Published Feb 1, 2014• 0 citations
OpenAlex

Related papers

A Coq-Based Infrastructure for Quantum Programming, Verification and Simulation

Wenxuan Tao, Gang Chen

Lecture notes in computer science•Jan 1, 2024•0 citations

Symbolic Reasoning About Quantum Circuits in Coq

Wenjun Shi, Qinxiang Cao, Yuxin Deng +2 more

arXiv:2005.11023•Journal of Computer Science and Technology•Nov 30, 2021•10 citations

Formal Verification of Robertson-Type Uncertainty Relation

Takaaki Masuhara, Toru KURIYAMA, M. Yoshida +1 more

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.

Journal of Quantum Information Science•Jan 1, 2015•1 citation

Equivalence Checking of Quantum Protocols

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

Lecture notes in computer science•Jan 1, 2013•35 citations

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

Robert W. Rand, Jennifer Paykin, Steve Zdancewic

We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.

arXiv:1803.00699•Electronic Proceedings in Theoretical Computer Science•Feb 27, 2018•72 citations

Verification of Concurrent Quantum Protocols by Equivalence Checking

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

Lecture notes in computer science•Jan 1, 2014•33 citations
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.
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.