Robert W. Rand
YOU?
Author Swipe
View article: A Language for Quantifying Quantum Network Behavior
A Language for Quantifying Quantum Network Behavior Open
Quantum networks have capabilities that are impossible to achieve using only classical information. They connect quantum capable nodes, with their fundamental unit of communication being the Bell pair , a pair of entangled quantum bits. Du…
View article: Compositional Quantum Control Flow with Efficient Compilation in Qunity
Compositional Quantum Control Flow with Efficient Compilation in Qunity Open
Most existing quantum programming languages are based on the quantum circuit model of computation, as higher-level abstractions are particularly challenging to implement—especially ones relating to quantum control flow. The Qunity language…
View article: An Algebraic Language for Specifying Quantum Networks
An Algebraic Language for Specifying Quantum Networks Open
Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair , which consists of two entangled quantum bits. …
View article: ViCAR: Visualizing Categories with Automated Rewriting in Coq
ViCAR: Visualizing Categories with Automated Rewriting in Coq Open
We present ViCAR, a library for working with monoidal categories in the Coq proof assistant. ViCAR provides definitions for categorical structures that users can instantiate with their own verification projects. Upon verifying relevant coh…
View article: VyZX: Formal Verification of a Graphical Quantum Language
VyZX: Formal Verification of a Graphical Quantum Language Open
Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define se…
View article: Q# as a Quantum Algorithmic Language
Q# as a Quantum Algorithmic Language Open
Q# is a standalone domain-specific programming language from Microsoft for writing and running quantum programs.Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its in…
View article: COGNAC: Circuit Optimization via Gradients and Noise-Aware Compilation
COGNAC: Circuit Optimization via Gradients and Noise-Aware Compilation Open
We present COGNAC, a novel strategy for compiling quantum circuits based on numerical optimization algorithms from scientific computing. Observing that shorter-duration "partially entangling" gates tend to be less noisy than the typical "m…
View article: A Verified Optimizer for Quantum Circuits
A Verified Optimizer for Quantum Circuits Open
We present voqc , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir , a small quantum intermediate representatio…
View article: A formally certified end-to-end implementation of Shor’s factorization algorithm
A formally certified end-to-end implementation of Shor’s factorization algorithm Open
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less…
View article: Qunity: A Unified Language for Quantum and Classical Computing
Qunity: A Unified Language for Quantum and Classical Computing Open
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum an…
View article: Qunity: A Unified Language for Quantum and Classical Computing (Type Checker)
Qunity: A Unified Language for Quantum and Classical Computing (Type Checker) Open
This code repository is designed to accompany the paper "Qunity: A Unified Language for Quantum and Classical Computing." You can run the "make" command to compile our proofs. See the README.md file for more details.
View article: Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective
Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective Open
Universal and fault-tolerant quantum computation is a promising new paradigm that may efficiently conquer difficult computation tasks beyond the reach of classical computation. It motivates the development of various quantum technologies. …
View article: Q# as a Quantum Algorithmic Language
Q# as a Quantum Algorithmic Language Open
Q# is a standalone domain-specific programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its i…
View article: VyZX : A Vision for Verifying the ZX Calculus
VyZX : A Vision for Verifying the ZX Calculus Open
Optimizing quantum circuits is a key challenge for quantum computing. The PyZX compiler broke new ground by optimizing circuits via the ZX calculus, a powerful graphical alternative to the quantum circuit model. Still, it carries no guaran…
View article: MCBeth: A Measurement Based Quantum Programming Language
MCBeth: A Measurement Based Quantum Programming Language Open
Gate-based quantum programming languages are ubiquitous but measurement-based languages currently exist only on paper. This work introduces MCBeth, a quantum programming language which allows programmers to directly represent, program, and…
View article: A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm Open
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a …
View article: Gottesman Types for Quantum Programs
Gottesman Types for Quantum Programs Open
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set H, S and CNOT. The Gottesman-Knill theorem showed tha…
View article: Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs Open
We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications includ…
View article: Static Analysis of Quantum Programs via Gottesman Types
Static Analysis of Quantum Programs via Gottesman Types Open
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set $H$, $S$ and $CNOT$. The Gottesman-Knill theorem show…
View article: A verified optimizer for Quantum circuits
A verified optimizer for Quantum circuits Open
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate represen…
View article: Proving Quantum Programs Correct
Proving Quantum Programs Correct Open
As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of …
View article: Verified Optimization in a Quantum Intermediate Representation
Verified Optimization in a Quantum Intermediate Representation Open
We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification proce…
View article: Verification Logics for Quantum Programs
Verification Logics for Quantum Programs Open
We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani…
View article: ReQWIRE: Reasoning about Reversible Quantum Circuits
ReQWIRE: Reasoning about Reversible Quantum Circuits Open
Common quantum algorithms make heavy use of ancillae: scratch qubits that are\ninitialized at some state and later returned to that state and discarded.\nExisting quantum circuit languages let programmers assert that a qubit has been\nretu…
View article: QWIRE Practice: Formal Verification of Quantum Circuits in Coq
QWIRE Practice: Formal Verification of Quantum Circuits in Coq Open
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem provin…
View article: Formally Verified Quantum Programming
Formally Verified Quantum Programming Open
The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger equation and the Church-Turing thesis. It took another fifty years for Feynman to recognize that harnessing…
View article: QWIRE: a core language for quantum circuits
QWIRE: a core language for quantum circuits Open
This paper introduces QWIRE (``choir''), a language for defining quantum circuits and an interface for manipulating them inside of an arbitrary classical host language. QWIRE is minimal---it contains only a few primitives---and sound with …
View article: QWIRE: a core language for quantum circuits
QWIRE: a core language for quantum circuits Open
This paper introduces QWIRE (``choir''), a language for defining quantum circuits and an interface for manipulating them inside of an arbitrary classical host language. QWIRE is minimal---it contains only a few primitives---and sound with …
View article: Feature analysis and reduction of laws texture measure
Feature analysis and reduction of laws texture measure Open
The Laws Texture Measure was tested in an autoevaluation experiment and compared to some of the texture measures previously studied. In addition, four methods of component reduction were evaluated. Laws Texture was found to be the most eff…