Current browse context:
quant-ph
Change to browse by:
References & Citations
Quantum Physics
Title: A Rich Type System for Quantum Programs
(Submitted on 22 Jan 2021 (v1), last revised 4 Feb 2022 (this version, v3))
Abstract: We show that Gottesman's semantics (GROUP22, 1998) for Clifford circuits based on the Heisenberg representation can be treated as a type system that can efficiently characterize a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bi-partition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) typing post-measurement states for computational basis measurements. Further, this type system is extended to accommodate universal quantum computing by deriving types for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. These types allow us to prove a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate.
Submission history
From: Robert Rand [view email][v1] Fri, 22 Jan 2021 04:07:12 GMT (35kb,D)
[v2] Fri, 17 Dec 2021 06:03:29 GMT (77kb,D)
[v3] Fri, 4 Feb 2022 05:33:54 GMT (86kb,D)
Link back to: arXiv, form interface, contact.