REVIEW 1 cited by
Runtime Analysis of Quantum Programs: A Formal Approach
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Runtime Analysis of Quantum Programs: A Formal Approach
read the original abstract
In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus \`a la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can be readily used to derive upper bounds of their runtime. Finally, we show the applicability of our calculus analyzing the runtime of (a simplified version of) the BB84 quantum key distribution protocol.
Forward citations
Cited by 1 Pith paper
-
Complex Bounded Operators in Isabelle/HOL
A comprehensive, machine-checked Isabelle/HOL formalization of complex Hilbert spaces and bounded operators, including adjoints, unitaries, projectors, the BLT extension theorem, Loewner order, and ℓ2 spaces.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.