Search Results

Documents authored by Hicks, Michael

Document
DOI: 10.4230/LIPIcs.ITP.2021.21
Proving Quantum Programs Correct

Authors: Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover’s algorithm and quantum phase estimation, a key component of Shor’s algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.
Cite as

Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hietala_et_al:LIPIcs.ITP.2021.21,
  author =	{Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Li, Liyi and Hicks, Michael},
  title =	{{Proving Quantum Programs Correct}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.21},
  URN =		{urn:nbn:de:0030-drops-139160},
  doi =		{10.4230/LIPIcs.ITP.2021.21},
  annote =	{Keywords: Formal Verification, Quantum Computing, Proof Engineering}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.12
Formal Verification vs. Quantum Uncertainty

Authors: Robert Rand, Kesha Hietala, and Michael Hicks

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

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.
Cite as

Robert Rand, Kesha Hietala, and Michael Hicks. Formal Verification vs. Quantum Uncertainty. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SNAPL.2019.12},
  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}
}
Document
DOI: 10.4230/DagRep.4.12.29
The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492)

Authors: Gilles Barthe, Michael Hicks, Florian Kerschbaum, and Dominique Unruh

Published in: Dagstuhl Reports, Volume 4, Issue 12 (2015)

Abstract
Increasingly, modern cryptography (crypto) has moved beyond the problem of secure communication to a broader consideration of securing computation. The past thirty years have seen a steady progression of both theoretical and practical advances in designing cryptographic protocols for problems such as secure multiparty computation, searching and computing on encrypted data, verifiable storage and computation, statistical data privacy, and more. More recently, the programming-languages (PL) community has begun to tackle the same set of problems, but from a different perspective, focusing on issues such as language design (e.g., new features or type systems), formal methods (e.g., model checking, deductive verification, static and dynamic analysis), compiler optimizations, and analyses of side-channel attacks and information leakage. This seminar helped to cross-fertilize ideas between the PL and crypto communities, exploiting the synergies for advancing the development of secure computing, broadly speaking, and fostering new research directions in and across both communities.
Cite as

Gilles Barthe, Michael Hicks, Florian Kerschbaum, and Dominique Unruh. The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492). In Dagstuhl Reports, Volume 4, Issue 12, pp. 29-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{barthe_et_al:DagRep.4.12.29,
  author =	{Barthe, Gilles and Hicks, Michael and Kerschbaum, Florian and Unruh, Dominique},
  title =	{{The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492)}},
  pages =	{29--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{12},
  editor =	{Barthe, Gilles and Hicks, Michael and Kerschbaum, Florian and Unruh, Dominique},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.12.29},
  URN =		{urn:nbn:de:0030-drops-50045},
  doi =		{10.4230/DagRep.4.12.29},
  annote =	{Keywords: Security, Theory, Languages}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact