BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of quantum protocols using Coq - Jaap Boender\, Middl
 esex University
DTSTART:20141114T160000Z
DTEND:20141114T170000Z
UID:TALK55910@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:Quantum computing and quantum communication are exciting areas
  of research\nat the intersection of physics and computer science\, which 
 have great\npotential for influencing the future development of informatio
 n processing\nsystems. Quantum cryptography\, in particular\, is well deve
 loped. Commercial\nQuantum Key Distribution systems are easily available a
 nd several QKD\nnetworks have been built in various parts of the world. Ho
 wever\, the\nsecurity of the protocols rely on information-theoretic proof
 s\, which may or\nmay not reflect actual system behaviour\, and testing of
  the implementations.\nWe present a novel framework for modelling and prov
 ing quantum protocols\nusing the proof assistant Coq. We provide a Coq lib
 rary for quantum bits\n(qubits)\, quantum gates\, and quantum measurement.
  We implement and prove a\nsimple quantum coin flipping protocol. As a ste
 p towards verifying practical\nquantum communication and security protocol
 s\, such as Quantum Key\nDistribution\, we support multiple qubits\, commu
 nication and entanglement. We\nfurther illustrate these concepts by modell
 ing the Quantum Teleportation\nProtocol\, which communicates the state of 
 an unknown quantum bit using only\na classical channel.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR