Formalization \textit{of} quantum protocols using Coq

MaRDI QIDQ5015189zbMATH OpenFDO

Authors Jaap P. Boender, Florian Kammüller, Rajagopal Nagarajan

Publication date 6 December 2021

Full work available at URL https://arxiv.org/abs/1511.01568, http://eptcs.web.cse.unsw.edu.au/paper.cgi?QPL2015.6

Mathematics Subject Classification ID

Quantum algorithms and complexity in the theory of computing (68Q12) Formalization of mathematics in connection with theorem provers (68V20) Quantum computation (81P68)

Recommendations

• Equivalence checking of quantum protocols
• Automated equivalence checking of concurrent quantum systems
• Verifying quantum communication protocols with ground bisimulation
• Specification and verification of quantum protocols
• Verification of quantum protocols with a probabilistic model-checker

Cites work

• A calculus of mobile processes. II
• An algebra of quantum processes
• An Update on Quantum Cryptography
• Bisimulation for quantum processes
• Communicating quantum processes
• Equivalence checking of quantum protocols
• Experimental realization of a quantum relay over a significant distance
• scientific article; zbMATH DE number 1579275 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Mathematical Knowledge Management
• Model checking quantum Markov chains
• Relations among quantum processes: bisimilarity and congruence
• Specification and verification of quantum protocols
• Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels
• The Four Colour Theorem: Engineering of a Formal Proof
• Types and typechecking for Communicating Quantum Processes
• Unconditional security in quantum cryptography

Cited in

(17)

• An automated deductive verification framework for circuit-building quantum programs
• A modeling and verification framework for optical quantum circuits
• Certified quantum computation in Isabelle/HOL
• Verification of quantum protocols with a probabilistic model-checker
• Formal verification of complex coherence protocols using symbolic state models
• Proof verification technology and elementary physics
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• Robust cryptography in the noisy-quantum-storage model
• Automated equivalence checking of concurrent quantum systems
• Application of quantum process calculus to higher dimensional quantum protocols
• Equivalence checking of quantum protocols
• Modelling and simulation of quantum teleportation and dense coding using predicate/transition-nets
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning
• A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
• Describing and animating quantum protocols
• Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information

Describes a project that uses

Uses Software

• C-CoRN
• Coq

This page was built for publication: Formalization \textit{of} quantum protocols using Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5015189)