3 citations · 7 across the 17 of their papers we have counts for
19 papers
QEDIA: Quantum Program Verification in Lean
Yuanjie, Ren, Zhicheng Zhang +4
Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classica…
Quantisation of Abstract Data Types
Mingsheng Ying, Zhicheng Zhang, Kean Chen
In this paper, we introduce a notion of abstract quantum data type within the framework of universal algebra. This notion provides an algebraic foundation for describing data abstr…
Resource Estimation for Fault-Tolerant Quantum Programs
Bonan Su, Yuan Feng, Li Zhou +1
Fault-tolerant quantum computation enables the deployment of practical quantum algorithms but incurs substantial overhead from error correction, making resource estimation a centra…
Reasoning about Continuous-Variable Quantum Systems
Tianshi Yu, Gilles Barthe, Minbo Gao +2
Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient computational framework…
Verifying Adversarial Robustness in Quantum Machine Learning: from theory to physical validation via a software tool
Ji Guan, Mingsheng Ying
As with classical neural networks, quantum machine learning (QML) models are vulnerable to small input perturbations that can significantly alter output predictions. Certifying the…
QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits
Zihao Li, Ji Guan, Mingsheng Ying
We present a tool QSeqSim, a Qiskit-integrated symbolic backend that fills the current gap of having no Qiskit-native support for simulating while-loop quantum programs and their i…
A Compilation Framework for Quantum Simulation of Non-unitary Dynamics
Qifan Huang, Minbo Gao, Li Zhou +1
Most quantum compilers assume programs are reversible unitary circuits. This fits closed-system algorithms, but not open-system simulation, where the natural program objects are qu…
Symbolic Specification and Reasoning for Quantum Data and Operations
Mingsheng Ying
In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time,…
Borrowing Dirty Qubits in Quantum Programs
Bonan Su, Li Zhou, Yuan Feng +1
Dirty qubits are ancillary qubits that can be borrowed from idle parts of a computation, enabling qubit reuse and reducing the demand for fresh, clean qubits-a resource that is typ…
Access Control Threatened by Quantum Entanglement
Zhicheng Zhang, Mingsheng Ying
Access control is a cornerstone of computer security that prevents unauthorised access to resources. In this paper, we study access control in quantum computer systems. We present…
Laws of Quantum Programming
Mingsheng Ying, Li Zhou, Gilles Barthe
In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum settin…
A Practical Quantum Hoare Logic with Classical Variables, I
Mingsheng Ying
In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanc…
An Interpretation of Bunched Logic for Reasoning about Heap-Manipulating Quantum Programs
Bonan Su, Li Zhou, Yuan Feng +1
We introduce heap manipulation into quantum programming languages to enable flexible quantum memory management, which in turn poses new challenges for reasoning about program corre…
Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
Zhicheng Zhang, Mingsheng Ying
Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of…
Measurement-based Verification of Quantum Markov Chains
Ji Guan, Yuan Feng, Andrea Turrini +1
Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains.…
Atomicity in Distributed Quantum Computing
Zhicheng Zhang, Mingsheng Ying
Atomicity is a ubiquitous assumption in distributed computing, under which actions are indivisible and appear sequential. In classical computing, this assumption has several theore…
Equivalence Checking of Parameterised Quantum Circuits
Xin Hong, Wei-Jia Huang, Wei-Chen Chien +4
Parameterised quantum circuits (PQCs) hold great promise for demonstrating quantum advantages in practical applications of quantum computation. Examples of successful applications…
Verification of Recursively Defined Quantum Circuits
Mingsheng Ying, Zhicheng Zhang
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed.…
Quantum Recursive Programming with Quantum Case Statements
Mingsheng Ying, Zhicheng Zhang
We introduce a novel scheme of quantum recursive programming, in which large unitary transformations, i.e. quantum gates, can be recursively defined using quantum case statements,…