License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SNAPL.2019.12
URN: urn:nbn:de:0030-drops-105558
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10555/
Go to the corresponding LIPIcs Volume Portal

Rand, Robert ; Hietala, Kesha ; Hicks, Michael

Formal Verification vs. Quantum Uncertainty

pdf-format:
LIPIcs-SNAPL-2019-12.pdf (1 MB)

Abstract

Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify quantum programs against their intended semantics. This is not enough. Verifying an idealized semantics against a real world quantum program doesn't allow you to confidently predict the program’s output. In order to have verification that works, you need both an error semantics related to the hardware at hand (this is necessarily low level) and certified compilation to the that same hardware. Once we have these two things, we can talk about an approach to quantum programming where we start by writing and verifying programs at a high level, attempt to verify properties of the compiled code, and repeat as necessary.

BibTeX - Entry

@InProceedings{rand_et_al:LIPIcs.SNAPL.2019.12,
  author =	{Rand, Robert and Hietala, Kesha and Hicks, Michael},
  title =	{{Formal Verification vs. Quantum Uncertainty}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{12:1--12:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2019/10555},
  URN =		{urn:nbn:de:0030-drops-105558},
  doi =		{10.4230/LIPIcs.SNAPL.2019.12},
  annote =	{Keywords: Formal Verification, Quantum Computing, Programming Languages, Quantum Error Correction, Certified Compilation, NISQ}
}

Keywords: Formal Verification, Quantum Computing, Programming Languages, Quantum Error Correction, Certified Compilation, NISQ
Collection: 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Issue Date: 2019
Date of publication: 11.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI