arXiv subjects

Qinxiang Cao

Publications and source records attributed to Qinxiang Cao.

21 records · Page 2Linked to original sources

arXiv2021

Symbolic Reasoning about Quantum Circuits in Coq

A quantum circuit is a computational unit that transforms an input quantum state to an output one. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

cs.PL↗

arXiv2021

Countability of Inductive Types Formalized in the Object-Logic Level

The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably many elements. In this paper, we formalize the syntax of first order inductive definitions in Coq and prove them countable, under some side conditions. Instead of writing a proof generator in a meta language, we develop an axiom-free proof in the Coq object logic. In other words, our proof is a dependently typed Coq function from the syntax of the inductive definition to the countability of the type. Based on this proof, we provide a Coq tactic to automatically prove the countability of concrete inductive types. We also developed Coq libraries for countability and for the syntax of inductive definitions, which have value on their own.

cs.LO↗

arXiv2019

Proof Pearl: Magic Wand as Frame

Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating implication is less widely used. This paper demonstrates that by using magic wand to express frames that relate mutable local portions of data structures to global portions, we can exploit its power while proofs are still easily understandable. Many useful separation logic theorems about partial data structures can now be proved by simple automated tactics, which were usually proved by induction. This magic-wand-as-frame technique is especially useful when formalizing the proofs by a high order logic. We verify binary search tree insert in Coq as an example to demonstrate this proof technique.

cs.PL↗