VLDB 2026 Research / reviewers in the wild / expert
Finn Voichick
dblp:239/9510
· DBLP profile ↗
6ranked-venue papers
2as first author
3since 2021 · last 2025
0000-0002-1913-4178ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 3 · 1 first-author · 3 since 2021Human-computer interaction and ubiquitous computing · 3 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Compositional Quantum Control Flow with Efficient Compilation in QunityabstractMost 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, proposed by Voichick et al., offered such an abstraction in the form of a quantum control construct, with great care taken to ensure that the resulting language is still realizable. However, Qunity lacked a working implementation, and the originally proposed compilation procedure was very inefficient, with even simple quantum algorithms compiling to unreasonably large circuits. In this work, we focus on the efficient compilation of high-level quantum control flow constructs, using Qunity as our starting point. We introduce a wider range of abstractions on top of Qunity’s core language that offer compelling trade-offs compared to its existing control construct. We create a complete implementation of a Qunity compiler, which converts high-level Qunity code into the quantum assembly language OpenQASM 3. We develop optimization techniques for multiple stages of the Qunity compilation procedure, including both low-level circuit optimizations as well as methods that consider the high-level structure of a Qunity program, greatly reducing the number of qubits and gates used by the compiler. Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, Robert Rand 0001 |
Proc. ACM Program. Lang. | 2 |
| 2023 | Qunity: A Unified Language for Quantum and Classical ComputingabstractWe 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 and classical effects. For example, one can use sum types to implement the direct sum of linear operators, exception-handling syntax to implement projective measurements, and aliasing to induce entanglement. Further, Qunity takes advantage of the overlooked BQP subroutine theorem, allowing one to construct reversible subroutines from irreversible quantum algorithms through the uncomputation of "garbage" outputs. Unlike existing languages that enable quantum aspects with separate add-ons (like a classical language with quantum gates bolted on), Qunity provides a unified syntax and a novel denotational semantics that guarantees that programs are quantum mechanically valid. We present Qunity's syntax, type system, and denotational semantics, showing how it can cleanly express several quantum algorithms. We also detail how Qunity can be compiled into a low-level qubit circuit language like OpenQASM, proving the realizability of our design. Finn Voichick, Liyi Li 0002, Robert Rand 0001, Michael Hicks 0001 |
Proc. ACM Program. Lang. | 1 |
| 2022 | Verified compilation of Quantum oraclesabstractQuantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM’s design enabled us to prove correct VQO’s compilers—from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language—and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor’s and Grover’s algorithms. We found that VQO’s QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using “classical” gates; VQO’s versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform. Liyi Li 0002, Finn Voichick, Kesha Hietala, Yuxiang Peng 0004, Xiaodi Wu 0001, Michael Hicks 0001 |
Proc. ACM Program. Lang. | 2 |
| 2020 | Exploring Programmers' API Learning Processes: Collecting Web Resources as External MemoryabstractModern programming frequently requires the use of APIs (Application Programming Interfaces). Yet many programmers struggle when trying to learn APIs. We ran an exploratory study in which we observed participants performing an API learning task. We analyze their processes using a proposed model of API learning, grounded in Cognitive Load Theory, Information Foraging Theory, and External Memory research. The results provide support for the model of API Learning and add new insights into the form and usage of external memory while learning APIs. Programmers quickly curated a set of API resources through Information Foraging which served as external memory and then primarily referred to these resources to meet information needs while coding. Gao Gao, Finn Voichick, Michelle Ichinco, Caitlin Kelleher |
VL/HCC | 2 |
| 2019 | The Long Tail: Understanding the Discoverability of API FunctionalityabstractAlmost all software development revolves around the discovery and use of application programming interfaces (APIs). Once a suitable API is selected, programmers must begin the process of determining what functionality in the API is relevant to a programmer's task and how to use it. Our work aims to understand how API functionality is discovered by programmers and where tooling may be appropriate. We employed a mixed-methods approach to investigate Apache Beam, a distributed data processing API, by mining Beam client code and running a lab study to see how people discover Beam's available functionality. We found that programmers' prior experience with similar APIs significantly impacted their ability to find relevant features in an API and attempting to form a top-down mental model of an API resulted in less discovery of features. Amber Horvath, Sachin Grover, Sihan Dong, Emily Zhou, Finn Voichick, Mary Beth Kery, Shwetha Shinju, Daye Nam, Mariann Nagy, Brad A. Myers |
VL/HCC | 5 |
| 2019 | Towards Validation of a Model of API LearningabstractAPIs (Application Programming Interfaces) and code libraries have become highly integrated into the programming process. They allow programmers to reuse large segments of functionalities. However, as free and often open-source commodities, the support for programmers to learn how to use these valuable resources is not always complete. Researchers have repeatedly found that API learning is a highly problematic process with many barriers. However, much of the work on the difficulties using and learning APIs has relied on retrospective descriptions of the process or questions programmers post on forums. Furthermore, these explorations of difficulties in learning APIs have not taken into account theories about learning or information foraging. In this works-in-progress poster, we present an early evaluation of a model that describes API learning using both information foraging and cognitive load theory. Finn Voichick, Gao Gao, Michelle Ichinco, Caitlin Kelleher |
VL/HCC | 1 |