



@article {2729,
	title = {Proving Quantum Programs Correct},
	journal = {Schloss Dagstuhl},
	year = {2021},
	month = {7/13/2021},
	abstract = {<p>As quantum computing steadily progresses from theory to practice, programmers are faced with 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 Simon\&$\#$39;s algorithm, Grover\&$\#$39;s algorithm, and quantum phase estimation, a key component of Shor\&$\#$39;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.</p>},
	doi = {https://doi.org/10.4230/LIPIcs.ITP.2021.21},
	url = {https://arxiv.org/abs/2010.01240},
	author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Liyi Li and Michael Hicks}
}
@article {2558,
	title = {On the Principles of Differentiable Quantum Programming Languages},
	year = {2020},
	month = {4/2/2020},
	abstract = {<p>Variational Quantum Circuits (VQCs), or the so-called quantum neural-networks, are predicted to be one of the most important near-term quantum applications, not only because of their similar promises as classical neural-networks, but also because of their feasibility on near-term noisy intermediate-size quantum (NISQ) machines. The need for gradient information in the training procedure of VQC applications has stimulated the development of auto-differentiation techniques for quantum circuits. We propose the first formalization of this technique, not only in the context of quantum circuits but also for imperative quantum programs (e.g., with controls), inspired by the success of differentiable programming languages in classical machine learning. In particular, we overcome a few unique difficulties caused by exotic quantum features (such as quantum no-cloning) and provide a rigorous formulation of differentiation applied to bounded-loop imperative quantum programs, its code-transformation rules, as well as a sound logic to reason about their correctness. Moreover, we have implemented our code transformation in OCaml and demonstrated the resource-efficiency of our scheme both analytically and empirically. We also conduct a case study of training a VQC instance with controls, which shows the advantage of our scheme over existing auto-differentiation for quantum circuits without controls.</p>},
	doi = {https://doi.org/10.1145/3385412.3386011},
	url = {https://arxiv.org/abs/2004.01122},
	author = {Shaopeng Zhu and Shih-Han Hung and Shouvanik Chakrabarti and Xiaodi Wu}
}
