



@article {2384,
	title = {Verification Logics for Quantum Programs},
	year = {2019},
	type = {Originally submitted in March 2016 as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania},
	abstract = {<p>We survey the landscape of Hoare logics for quantum programs. We review three papers: \&quot;Reasoning about imperative quantum programs\&quot; by Chadha, Mateus and Sernadas; \&quot;A logic for formal verification of quantum programs\&quot; by Yoshihiko Kakutani; and \&quot;Floyd-hoare logic for quantum programs\&quot; 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.</p>},
	url = {https://arxiv.org/abs/1904.04304},
	author = {Robert Rand}
}
