Workshop Details

 In this talk, we will introduce a new scheme of quantum recursive programing with quantum if-statement. A simple programming language for supporting this kind of quantum recursion is defined, and its semantics is formally described. A series of examples are presented to show that some quantum algorithms can be elegantly written as quantum recursive programs. At the end, we will briefly discuss verification and compilation of quantum recursive programs.   

Speaker Bio: Mingsheng Ying is a Distinguished Professor at the Centre for Quantum Software and Information, University of Technology Sydney, Australia. His research interests include quantum computing, programming theory, and logics in artificial intelligence. He has authored the books Model Checking Quantum Systems: Principles and Algorithms (Cambridge University Press, 2021), Foundations of Quantum Programming (Morgan Kaufmann, 2016), and Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs (Springer-Verlag, 2001). He currently serves as the inaugural (Co-)Editor-in-Chief of the ACM Transactions on Quantum Computing.

Bringing the promise of quantum computation into reality requires not only building a quantum computer but also correctly programming it to run a quantum algorithm. To obtain asymptotic advantage over classical algorithms, quantum algorithms rely on the ability of data in quantum superposition to exhibit phenomena such as interference and entanglement. In turn, an implementation of the algorithm as a program must correctly orchestrate these phenomena in the states of qubits. Otherwise, the algorithm would yield incorrect outputs or lose its computational advantage.

Given a quantum algorithm, what are the challenges and costs to realizing it as a program that can run on a physical quantum computer? In this talk, I answer this question by showing how basic programming abstractions upon which many quantum algorithms rely – such as data structures and control flow – can fail to work correctly or efficiently on a quantum computer. I then show how we can leverage insights from programming languages to re-invent the software stack of abstractions, libraries, and compilers to meet the demands of quantum algorithms. This approach holds out a promise of expressive and efficient tools to program a quantum computer and practically realize its computational advantage.

Speaker bio: Charles Yuan is an incoming Assistant Professor at the University of Wisconsin, Madison and currently a Ph.D. candidate at MIT CSAIL advised by Prof. Michael Carbin. His research examines the challenges of programming quantum computers and other emerging models of computation. His work has appeared in the ACM SIGPLAN POPL, OOPSLA, and PLDI conferences and has been recognized with the SIGPLAN Distinguished Artifact Award and the CQE-LPS Doc Bedard Fellowship.

Cloud computing services offer time on quantum computers, but users are forced to each use the entire quantum computer to run their programs as there is no way to multiplex a quantum computer among multiple programs at the same time. We present HyperQ, a system that introduces virtual machines for quantum computers to provide fault isolation, better resource utilization, and lower latency for quantum cloud computing. A quantum virtual machine is defined in terms of quantum computer hardware, specifically its quantum gates and qubits arranged in a hardware-specific topology. HyperQ enables quantum virtual machines to be simultaneously executed together on a quantum computer by multiplexing them in time and space on the hardware and ensuring that they are isolated from one another. HyperQ works with existing quantum programs and compiler frameworks; programs are simply compiled to run in virtual machines without the programs or compilers needing to know what else might be executed at the same time. We have implemented HyperQ for the IBM quantum computing service, the largest quantum computing fleet in the world. Our experimental results running quantum programs in virtual machines using the IBM service demonstrate that HyperQ can increase utilization and throughput while reducing program latency, by up to an order of magnitude, without sacrificing, and in some cases improving, fidelity in the results of quantum program execution.

Speaker bio: Runzhou Tao is an Assistant Professor of Computer Science and a Fellow of the Joint Center for Quantum Information and Computer Science at the University of Maryland, College Park. He earned his Ph.D. in Computer Science from Columbia University in 2024 and his Bachelor’s degree from the Yao Class at Tsinghua University. His research explores the intersection of programming languages, operating systems, and quantum computing.

We seek to verify the ZX-calculus, a powerful tool for representing and reasoning about quantum computation. ZX-diagrams are typically represented as adjacency-based graphs, reflecting the guiding principle that “only connectivity matters”. In the context of formal theorem provers like Coq, however, such graphs are difficult to reason about, especially when we seek to give them semantics. To address this gap, we introduce VyZX, a verified library for reasoning about the ZX-calculus, using inductive constructs that arise naturally from category theoretic definitions. We extend VyZX to reason about a variety of monoidal categories, provided they satisfy an appropriate set of coherence conditions, and show how to automate highly graphical proofs.

Speaker bio: Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. His research focuses on programming languages and verification for quantum computing and his main projects include the VOQC compiler for quantum circuits, the BellKAT quantum network language, and VyZX, a verified ZX calculus library. He also works on a range of verification projects, from adding automation to the Rocq proof assistant to developing quantum program logics. Robert developed and maintains the INQWIRE QuantumLib, an open-source library for verified quantum computing in Rocq, which underlies many of his projects including his online textbook, Verified Quantum Computing.

To build a large-scale fault-tolerant quantum computer, quantum low-density parity-check (LPDC) codes have been established as promising candidates for low-overhead memory when compared to the surface codes. Performing logical computation on QLDPC memory, however, has been a long-standing challenge in theory and in practice.

In this work, we propose a new primitive, which we call an extractor, that can augment any QLDPC memory into a computational block well-suited for Pauli-based computation. In particular, any logical Pauli operator supported on the memory can be fault-tolerantly measured in one logical cycle, consisting of O(d) physical syndrome measurement cycles, without rearranging qubit connectivity.  We further propose the extractor architecture, which is a fixed-connectivity, LDPC architecture built by connecting many extractor-augmented computational (EAC) blocks with bridge systems. When combined with any source of high fidelity

Joint work with Alexander Cowtan, Dominic Williamson and Theodore Yoder: arxiv.org/abs/2503.10390.

Quantum computers can efficiently solve problems which are widely believed to lie beyond the reach of classical computers. In the near-term, hybrid quantum-classical algorithms, which efficiently embed quantum hardware in classical frameworks, are crucial in bridging the vast divide in the performance of the purely-quantum algorithms and their classical counterparts. Here, a hybrid quantum-classical algorithm is presented for the computation of non-perturbative characteristics of quantum field theories. The presented algorithm relies on a universal parametrized quantum circuit ansatz based on Euler and Cartan's decompositions of single and two-qubit operators. It is benchmarked by computing the energy spectra of lattice realizations of quantum field theories with both short and long range interactions. Low depth circuits are provided for false vacua as well as highly excited states corresponding to mesonic and baryonic excitations occurring in the analyzed models.

Speaker Bio:

• August 2024 – present: Research Staff (part-time), Condensed Matter and Materials Science Division, Brookhaven National Laboratory, USA
• September 2021 – present: Assistant Professor, Rutgers University, USA
• December 2018 – August 2021: Postdoctoral researcher, Technical University Munich, Germany
• June 2018 – November 2018: Visiting researcher, CEA Saclay, France
• September 2016 – May 2018: Postdoctoral researcher, RWTH Aachen University, Germany
• September 2010 – August 2016: PhD student, Yale University

This paper addresses the problem of checking whether two constant-depth (shallow) quantum circuits are functionally equivalent—a key task in verifying circuit transformations. Since directly simulating quantum states can be exponentially expensive, the paper introduces efficient classical decision procedures for two variants of the equivalence-checking problem. The key idea is to use local projections as constraints that uniquely determine the output state of a shallow circuit. This avoids computing the full state explicitly. The approach also enables sound and complete assertion checking for conjunctions of local projections. Experiments show practical performance: e.g., checking equivalence for 100-qubit, depth-3 circuits takes under 32 seconds.

Speaker bio: Nengkun Yu is a faculty member in the Department of Computer Science at Stony Brook University. He received both his Bachelor's and Ph.D. degrees from Tsinghua University. Before joining Stony Brook, he was affiliated with the University of Technology Sydney. His research interests lie in quantum learning and quantum programming. His work has been recognized with two ACM SIGPLAN Distinguished Paper Awards, at OOPSLA and PLDI, respectively.

Abstract: In this talk, I will present recent progress on quantum signal processing (QSP) algorithms on hybrid continuous-discrete-variable (CV-DV) quantum processors, and highlight its potential to serve as a universal framework to design modular quantum software systems. I will start by introducing instruction set architecture on hybrid quantum processors. Quantum state transfer and quantum Fourier transform will follow as an example to illustrate the application. I will conclude with open problems and future opportunities towards building modular quantum software systems based on QSP.

Speaker bio: Yuan Liu is an Assistant Professor of Electrical & Computer Engineering and Computer Science at North Carolina State University. He is also an affiliated faculty in Physics. He received his B.S. in physics from Tsinghua University, M.S. in electrical engineering and a Ph.D. in chemical physics from Brown University. Prior to joining NC State faculty, he was a postdoctoral researcher in the Research Laboratory of Electronics and Department of Physics at MIT. His research interests lie at the intersection of quantum computing, theoretical chemistry and physics, and quantum engineering.

Assertions are used extensively in classical programming to check for program bugs or runtime errors. In quantum computers, runtime error rates are typically many orders of magnitude higher than error rates in classical computing, making it critical to detect such errors. The problem is exacerbated due to several factors. The first is that we cannot observe quantum information without destroying it, and the second is that the process of detecting errors can itself introduce extra errors.

In this talk I will discuss error detection in quantum circuits dominated by Clifford gates, and show algorithms for finding good checks even in the presence of severe qubit connectivity constraints. The key idea is to use spacetime codes to probe for errors more efficiently. Such checks introduce little overhead and can in turn detect errors in a large region of the circuit. I will show the practicality of the approach by showing experimental results on IBM Quantum processors for circuits containing up to 50 logical qubits and close to 2,500 two-qubit gates. I will argue that such error detection methods form a viable bridge between near-term error mitigation and longer-term error correction in quantum computers.

Speaker bio: Ali Javadi-Abhari is a Principal Research Scientist at IBM Quantum. His research interests lie in quantum circuits and compilation. He was the architect of the Qiskit software framework for quantum information science, and led the software sub-thrust of the C2QA center of the National Quantum Initiative. He received his PhD from Princeton University in 2017.

Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.

Speaker bio: Kean Chen is currently a postdoctoral researcher at the Department of Computer and Information Science, University of Pennsylvania, USA. His research focuses on quantum error correction and quantum information.

Stabilizer circuits are classically tractable quantum circuits that are widely used by architects and theorists to design and benchmark protocols at scale. Despite their attractive properties and a rich body of applications, there have been no qudit stabilizer simulators for 𝑑 > 2. We introduce the first realization of such a simulator modeled after CHP and stim. We validate its correctness and demonstrate its usefulness via a qudit randomized benchmarking case study that supports a physical experiment. This abstraction will be the indispensable tool for novel qudit error correction, as earlier stabilizer simulators have been for qubits.

Speaker bio: Yipeng Huang is an assistant professor of computer science at Rutgers. His research and teaching are in the software-hardware interface of computers, broadly defined: digital, analog, and quantum. He is interested abstractions that make programming these computers easier, and in building simulators and tools that allow for automated validation and characterization. His work has appeared at ACM and IEEE's conferences on computer architecture and has been named among the top picks on several occasions.

The rapid progress in quantum hardware is expected to make them viable tools for the study of quantum algorithms in the near term. To accelerate the timeline of useful algorithmic experimentation, one effective technique is to encode the quantum circuit using an error detection code and discard the samples for which an error has been detected. An under-explored property of error-detecting codes is the flexibility in the circuit encoding and fault-tolerant gadgets, which enables their co-optimization with the algorithmic circuit, which is not available for standard circuit optimization tools. In this work, we focus on the [[k+2, k, 2]] Iceberg quantum error detection code and design new flexible fault-tolerant gadgets for it, which we then co-optimize with the quantum approximate optimization algorithm (QAOA) circuit using tree search. By co-optimizing the QAOA circuit and the Iceberg gadgets, we achieve an improvement in QAOA success probability from 44% to 65% and an increase in post-selection rate from 4% to 33% at 22 algorithmic qubits. Furthermore, we demonstrate better-than- unencoded performance for up to 34 algorithmic qubits, employing 510 algorithmic two-qubit gates and 1140 physical two-qubit gates on the Quantinuum H2-1 quantum computer. In addition, we will present an analytical model to characterize the applicability of quantum error detection code on the QAOA circuit and predict its performance in the future device.

Speaker bio: Dr. Zichang He is the Applied Research Lead (Vice President) at the Global Technology Applied Research Center at JPMorganChase. He earned his Ph.D. in Electrical and Computer Engineering from the University of California, Santa Barbara, in 2023. His research primarily focuses on quantum computing and its design automation. He is the recipient of the IEE Excellence in Research Fellowship at UCSB and has received two Best Student Paper Awards at IEEE conferences.

Chaotic evolution, the exponential sensitivity to initial conditions, underpins a great deal of everyday phenomena. In certain settings, it is possible to control the chaotic evolution by pushing the system towards an unstable fixed point of the dynamics, which drives the system through an absorbing state transition. Recent efforts have shown how to embed this dynamics into a quantum many body system, which requires using measurements and feedback to design the control operation. In the quantum setting this drives a measurement induced phase transition that may or may not coincide with the absorbing state transition depending on the structure of the feedback operation. We will discuss the current theoretical understanding of feedback driven transitions in quantum many-body systems and will present data on realizing this system on IBM’s superconducing quantum processor with over 100 qubits.

Quantum computing imposes stringent requirements for the precise control of large-scale qubit systems, including, for example, microsecond-latency feedback and nanosecond-precision timing of gigahertz signals—demands that far exceed the capabilities of conventional real-time systems. The rapidly evolving and highly diverse nature of quantum control necessitates the development of specialized hardware accelerators. While a few custom real-time systems have been developed to meet the tight timing constraints of specific quantum platforms, they face major challenges in scaling and adapting to increasingly complex control demands—largely due to fragmented toolchains and limited support for design automation.

To address these limitations, we present RISC-Q—an open-source flexible generator for Quantum Control System-on-Chip (QCSoC) designs, featuring a programming interface compatible with the RISC-V ecosystem. Developed using SpinalHDL, RISC-Q enables efficient automation of highly parameterized and modular QCSoC architectures, supporting agile and iterative development to meet the evolving demands of quantum control. We demonstrate that RISC-Q can replicate the performance of existing QCSoCs with significantly reduced development effort, facilitating efficient exploration of the hardware–software co-design space for rapid prototyping and customization.

Speaker bio: Junyi Liu is a postdoctoral scholar at the QuICS, University of Maryland, advised by Xiaodi Wu. He received his Ph.D. in computer science from the Institute of Software, Chinese Academy of Sciences, under the supervision of Prof. Mingsheng Ying. His expertise lies in the analysis and verification of quantum software. His current focus is on designing software and hardware infrastructure to enhance the performance and accessibility of quantum devices.

Circuit quantum electrodynamics (cQED) with superconducting cavities coupled to nonlinear elements such as transmons offers a powerful platform for quantum information processing, combining long cavity coherence times with the benefits of bosonic error correction. Multimode cQED architectures further enhance hardware efficiency and connectivity, enabling gate operations between arbitrary pairs of cavity modes using only a few control lines.
However, these systems face key challenges, including ancilla-induced crosstalk and decoherence, as well as cavity errors from ancilla backaction and the inverse Purcell effect—issues that become more pronounced as cavity coherence improves.
In this talk, I will present recent experimental implementations of strategies to mitigate ancilla-induced errors by weakening dispersive coupling while preserving fast gate speeds through ancilla displacements. Using sideband drives, we realize a tunable Jaynes–Cummings interaction between a transmon and any cavity mode, enabling SWAP gates nearly 40× faster than those in the