Mingsheng Ying

A Theorem Prover for Quantum Hoare Logic and Its Applications

2016 · arXiv (Cornell University)

Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying …

$Q|SI\rangle$: A Quantum Programming Environment

2017 · arXiv (Cornell University)

This paper describes a quantum programming environment, named $Q|SI\rangle$. It is a platform embedded in the .Net language that supports quantum programming using a quantum extension of the $\mathbf{while}$-language. The framework of the platform includes …

Super-activating quantum memory with entanglement

2018 · Quantum Information and Computation

Noiseless subsystems were proved to be an efficient and faithful approach to preserve fragile information against decoherence in quantum information processing and quantum computation. They were employed to design a general (hybrid) quantum memory cell …

Relational proofs for quantum programs

2020 · UTS ePRESS (University of Technology Sydney)

© 2020 Copyright held by the owner/author(s). Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation …

Control Flow Adaption: An Efficient Simulation Method For Noisy Quantum Networks

2024 · arXiv (Cornell University)

Quantum network research at both the software stack and hardware implementation level has become an exciting area of quantum information science. Although demonstrations of small-scale quantum networks have emerged in the past decade, quantum communication …