@inproceedings{Boender2015,
  title     = {Formalization of Quantum Protocols using Coq},
  author    = {Boender, Jaap and Kamm{\"u}ller, Florian and Nagarajan, Rajagopal},
  year      = {2015},
  month     = nov,
  booktitle = {Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, U.K., July 15--17, 2015},
  editor    = {Heunen, Chris and Selinger, Peter and Vicary, Jamie},
  publisher = opa,
  address   = {Waterloo, NSW, Australia},
  series    = eptcs,
  volume    = {195},
  pages     = {71--83},
  doi       = {10.4204/EPTCS.195.6},
  abstract  = {Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great potential for influencing the future development of information processing systems. The building of practical, general purpose Quantum Computers may be some years into the future. However, Quantum Communication and Quantum Cryptography are well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. The security of the protocols used in these implementations rely on information-theoretic proofs, which may or may not reflect actual system behaviour. Moreover, testing of implementations cannot guarantee the absence of bugs and errors. This paper presents a novel framework for modelling and verifying quantum protocols and their implementations using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. As a step towards verifying practical quantum communication and security protocols such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.},
  bibsource = qplbib
}

{"_id":"WgLXrSCRHdCb4i77J","bibbaseid":"boender-kammller-nagarajan-formalizationofquantumprotocolsusingcoq-2015","author_short":["Boender, J.","Kammüller, F.","Nagarajan, R."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Formalization of Quantum Protocols using Coq","author":[{"propositions":[],"lastnames":["Boender"],"firstnames":["Jaap"],"suffixes":[]},{"propositions":[],"lastnames":["Kammüller"],"firstnames":["Florian"],"suffixes":[]},{"propositions":[],"lastnames":["Nagarajan"],"firstnames":["Rajagopal"],"suffixes":[]}],"year":"2015","month":"November","booktitle":"Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, U.K., July 15–17, 2015","editor":[{"propositions":[],"lastnames":["Heunen"],"firstnames":["Chris"],"suffixes":[]},{"propositions":[],"lastnames":["Selinger"],"firstnames":["Peter"],"suffixes":[]},{"propositions":[],"lastnames":["Vicary"],"firstnames":["Jamie"],"suffixes":[]}],"publisher":"Open Publishing Association","address":"Waterloo, NSW, Australia","series":"Electronic Proceedings in Theoretical Computer Science","volume":"195","pages":"71–83","doi":"10.4204/EPTCS.195.6","abstract":"Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great potential for influencing the future development of information processing systems. The building of practical, general purpose Quantum Computers may be some years into the future. However, Quantum Communication and Quantum Cryptography are well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. The security of the protocols used in these implementations rely on information-theoretic proofs, which may or may not reflect actual system behaviour. Moreover, testing of implementations cannot guarantee the absence of bugs and errors. This paper presents a novel framework for modelling and verifying quantum protocols and their implementations using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. As a step towards verifying practical quantum communication and security protocols such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@inproceedings{Boender2015,\n title = {Formalization of Quantum Protocols using Coq},\n author = {Boender, Jaap and Kamm{\\\"u}ller, Florian and Nagarajan, Rajagopal},\n year = {2015},\n month = nov,\n booktitle = {Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, U.K., July 15--17, 2015},\n editor = {Heunen, Chris and Selinger, Peter and Vicary, Jamie},\n publisher = opa,\n address = {Waterloo, NSW, Australia},\n series = eptcs,\n volume = {195},\n pages = {71--83},\n doi = {10.4204/EPTCS.195.6},\n abstract = {Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great potential for influencing the future development of information processing systems. The building of practical, general purpose Quantum Computers may be some years into the future. However, Quantum Communication and Quantum Cryptography are well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. The security of the protocols used in these implementations rely on information-theoretic proofs, which may or may not reflect actual system behaviour. Moreover, testing of implementations cannot guarantee the absence of bugs and errors. This paper presents a novel framework for modelling and verifying quantum protocols and their implementations using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. As a step towards verifying practical quantum communication and security protocols such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.},\n bibsource = qplbib\n}\n\n","author_short":["Boender, J.","Kammüller, F.","Nagarajan, R."],"editor_short":["Heunen, C.","Selinger, P.","Vicary, J."],"key":"Boender2015","id":"Boender2015","bibbaseid":"boender-kammller-nagarajan-formalizationofquantumprotocolsusingcoq-2015","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":[],"search_terms":["formalization","quantum","protocols","using","coq","boender","kammüller","nagarajan"],"title":"Formalization of Quantum Protocols using Coq","year":2015}