activity
20202025
most citedGottesman Types for Quantum Programs

10 citations · 22 across the 10 of their papers we have counts for

collaborators

10 papers

quant-ph2025

Helios: A 98-qubit trapped-ion quantum computer

Anthony Ransford, M. S. Allman, Jake Arkinstall +183

We report on Quantinuum Helios, a 98-qubit trapped-ion quantum processor based on the quantum charge-coupled device (QCCD) architecture. Helios features Ba hyperfine…

quant-ph2025

Realization of a Quantum Streaming Algorithm on Long-lived Trapped-ion Qubits

Pradeep Niroula, Shouvanik Chakrabarti, Steven Kordonowy +30

Large classical datasets are often processed in the streaming model, with data arriving one item at a time. In this model, quantum algorithms have been shown to offer an unconditio…

quant-ph2025

Certified randomness amplification by dynamically probing remote random quantum states

Minzhao Liu, Pradeep Niroula, Matthew DeCross +49

Cryptography depends on truly unpredictable numbers, but physical sources emit biased or correlated bits. Quantum mechanics enables the amplification of imperfect randomness into n…

cs.PL2025

Imperative Quantum Programming with Ownership and Borrowing in Guppy

Mark Koch, Agustín Borgna, Craig Roy +4

Linear types enforce no-cloning and no-deleting theorems in functional quantum programming. However, in imperative quantum programming, they have not gained widespread adoption. Th…

cs.PL2025

GUPPY: Pythonic Quantum-Classical Programming

Mark Koch, Alan Lawrence, Kartik Singhal +2

We present ongoing work on Guppy, a domain-specific language embedded in Python that allows users to write high-level hybrid quantum programs with complex control flow in Pythonic…

cs.PL2022★ 7 cited

Q# as a Quantum Algorithmic Language

Kartik Singhal, Kesha Hietala, Sarah Marshall +1

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 sp…

cs.PL2021★ 3 cited

Quantum Hoare Type Theory: Extended Abstract

Kartik Singhal, John Reppy

As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verifica…

cs.LO2021★ 10 cited

Gottesman Types for Quantum Programs

Robert Rand, Aarthi Sundaram, Kartik Singhal +1

The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Cliffor…

quant-ph2021

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Aarthi Sundaram, Robert Rand, Kartik Singhal +2

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…

cs.PL2020★ 2 cited

Quantum Hoare Type Theory

Kartik Singhal

As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classi…