We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Quantum Physics

Title: Quantum Hoare Logic with Ghost Variables

Abstract: Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.
Subjects: Quantum Physics (quant-ph); Logic in Computer Science (cs.LO)
Cite as: arXiv:1902.00325 [quant-ph]
  (or arXiv:1902.00325v1 [quant-ph] for this version)

Submission history

From: Dominique Unruh [view email]
[v1] Fri, 1 Feb 2019 13:47:09 GMT (197kb)

Link back to: arXiv, form interface, contact.