Junyi Liu

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition . Then, we show that the expected runtime of a quantum program should be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. ( STOC 2001) is solved.

We propose a series of quantum algorithms for computing a wide range of quantum entropies and distances, including the von Neumann entropy, quantum Rényi entropy, trace distance, and fidelity. The proposed algorithms significantly outperform the prior best (and even quantum) ones in the low-rank case, some of which achieve exponential speedups. In particular, for N -dimensional quantum states of rank r , our proposed quantum algorithms for computing the von Neumann entropy, trace distance and fidelity within additive error ε have time complexity of Õ( r /ε ² ), Õ( r ⁵ /ε ⁶ ) and Õ( r ^6.5 /ε ^7.5 ), respectively. By contrast, prior quantum algorithms for the von Neumann entropy and trace distance usually have time complexity Ω( N ), and the prior best one for fidelity has time complexity Õ( r ^12.5 /ε ^13.5 ). The key idea of our quantum algorithms is to extend block-encoding from unitary operators in previous work to quantum states (i.e., density operators). It is realized by developing several convenient techniques to manipulate quantum states and extract information from them. The advantage of our techniques over the existing methods is that no restrictions on density operators are required; in sharp contrast, the previous methods usually require a lower bound on the minimal non-zero eigenvalue of density operators.

We introduce isQ, a new software stack for quantum programming in an imperative programming language, also named isQ. The aim of isQ is to make programmers write quantum programs as conveniently as possible. In particular: 1)The isQ language and its compiler contain many useful features, including but not limited to: classical control flow, such as recursion; decomposition of self-defined unitary gates; and oracle programming and its circuit realization. 2)To make it flexible, an isQ program can be compiled into several different kinds of intermediate representation and assemblies, including QIR, eQASM, OpenQASM 3.0, and QCIS (specially tailored for the superconducting quantum hardware at USTC). 3)Besides interfacing isQ with real superconducting hardware, a QIR simulator is also developed for the demonstration and testing of isQ programs. isQ software stack encompasses abundant compiler optimizations of high-level quantum programs. To realize it, a distinct MLIR dialect name isQ-IR is proposed.

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.