Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Reasoning about General Quantum Programs over Mixed States

Juliana Kaizer Vizzotto, Giovani Rubert Librelotto, Amr Sabry

Published Jan 1, 2009• 5 citations
Publisher
DOI
10.1007/978-3-642-10452-7_22

Related papers

Towards Efficient Reasoning of Quantum Programs

Nengkun Yu

Lecture notes in computer science•Jan 1, 2022•1 citation

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing

Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka +1 more

Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.

cs.PLCross-listedarXiv:2511.23472•Proceedings of the ACM on Programming Languages•Dec 1, 2025•2 citations

Analysis of quantum programs

Mingsheng Ying

Elsevier eBooks•Jan 1, 2024•2 citations

Non-deterministic quantum programming

Paolo Zuliani

In standard computation, non-determinism is used for specifying programs’ behaviour, without having to specify details of implementation. In quantum computation, non-determinism is either meant to be “classical” probabilism or it is not considered at all, since quantum computation is the physical theory of computation and thus it does not deal with non-implementable features. In this work we will instead show that non-determinism may be useful also in quantum computation. In particular, we consider non-determinism embedded in a programming language for quantum computation, the quantum Guarded-Command Language (qGCL), and use that for describing and reasoning about counterfactual computation and mixed-state systems.

•Dec 31, 2004•19 citations

Logic for quantum programs

Mingsheng Ying

Elsevier eBooks•Jan 1, 2016•28 citations

Towards the Dynamic Learning of an Experimental Entanglement Witness

Elizabeth Behrman, James E. Steck, P. K. Gagnebin +1 more

We present a dynamic learning paradigm for "programming" a general quantum computer. A learning algorithm is used to find the control parameters for a coupled qubit system, such that the system at an initial time evolves to a state in which a given measurement corresponds to the desired operation. We apply the method to a system of coupled superconducting quantum interference devices (SQUIDs), and demonstrate learning of the XOR, XNOR, Toffoli, and Fredkin gates. Striking out for more interesting territory, we attempt learning of an entanglement witness for a two qubit system. Simulation shows a reasonably successful mapping of the entanglement at the initial time onto the correlation function at the final time for both pure and mixed states. For pure states this mapping requires knowledge of the phase relation between the parts; however, given that knowledge, this method can be used to measure the entanglement of an unknown state.

IEEE Congress on Evolutionary Computation (CEC)•Sep 22, 2006•1 citation
Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.
In standard computation, non-determinism is used for specifying programs’ behaviour, without having to specify details of implementation. In quantum computation, non-determinism is either meant to be “classical” probabilism or it is not considered at all, since quantum computation is the physical theory of computation and thus it does not deal with non-implementable features. In this work we will instead show that non-determinism may be useful also in quantum computation. In particular, we consider non-determinism embedded in a programming language for quantum computation, the quantum Guarded-Command Language (qGCL), and use that for describing and reasoning about counterfactual computation and mixed-state systems.
We present a dynamic learning paradigm for "programming" a general quantum computer. A learning algorithm is used to find the control parameters for a coupled qubit system, such that the system at an initial time evolves to a state in which a given measurement corresponds to the desired operation. We apply the method to a system of coupled superconducting quantum interference devices (SQUIDs), and demonstrate learning of the XOR, XNOR, Toffoli, and Fredkin gates. Striking out for more interesting territory, we attempt learning of an entanglement witness for a two qubit system. Simulation shows a reasonably successful mapping of the entanglement at the initial time onto the correlation function at the final time for both pure and mixed states. For pure states this mapping requires knowledge of the phase relation between the parts; however, given that knowledge, this method can be used to measure the entanglement of an unknown state.