HackerPapers

arXiv:1904.04304cs.LO

Verification Logics for Quantum Programs

Robert Rand

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

Abstract

We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.

arXiv comments
Originally submitted in March 2016 as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science cs.ETEmerging Technologies cs.PLProgramming Languages

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Apr 2019 to Apr 2019. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.