Skip to content Skip to main navigation Report an accessibility issue

Workshop on Higher Category Approach to Certifiably Correct Quantum Information Processing Systems

This one-day Workshop is by invitation only. Send a message to if you wish to receive an invitation to participate. Limited funding is available for all participants. The Workshop will bring together mathematicians, logicians, physicists, and computer scientists, and is expected to be an important event toward the exploration of synergies between higher category theory, topological quantum field theories and quantum information processing, and a catalyst in the development of mathematical tools that will advance these synergies. It will also be attended by program managers looking for input to determine future topics of Multidisciplinary University Research Initiatives (MURIs) by the Department of Defense. Attendees will present their work, suggest future directions, and participate in discussions.

Date: Monday, February 4, 2019.

Venue: Sheraton College Park North Hotel.
Participants need to make their own reservations and then get reimbursed.

Reimbursements: Please address questions about reimbursements to Maria Fawver (e-mail:, phone: 865-974-3342).


8:00 – 8:30 Registration/Breakfast
8:30 – 8:40 Opening Address, Radhakrishnan Balu, Army Research Laboratory
8:40 – 9:00 George Siopsis, University of Tennessee

Hybrid Quantum Classical Algorithms

I discuss recent work on hybrid quantum classical algorithms with an eye towards implementation on quantum hardware in the near future. I concentrate on applications to quantum field theory, quantum communications, and machine learning.

9:00 – 9:30

Norbert Matthias Linke, University of Maryland

The first applications of near-term quantum computers will likely involve optimization tasks in a quantum-classical hybrid approach, where the quantum hardware is combined with a classical optimization algorithm. I will present recent results from such a hybrid system based on a trapped-ion quantum computer. Our experimental system is comprised of a chain of 171Yb+ ions with individual Raman beam addressing and individual readout. This fully connected processor can be configured to run any sequence of single- and two-qubit gates, making it an arbitrarily programmable quantum computer [1]. We combine this device with a classical optimizer which varies the quantum circuit parameters and interprets the results. This hybrid system is used to demonstrate the training of shallow circuits for generative modelling [2]. We contrast the use of different classical strategies for the training task, in particular particle-swarm and Bayesian optimization. Methods for scaling up this system will also be discussed.
[1] S. Debnath et al. Nature 536 63 (2016).
[2] D. Zhu et al. arXiv:1812.08862.
9:30 – 10:00
Emily Riehl, Johns Hopkins University
By expert consensus, the standard “analytic” techniques used to prove theorems about ∞-categories are too hard. We argue that if the current set-based foundations for mathematics were replaced with a new “univalent” foundation system known as homotopy type theory, the theory of ∞-categories could be developed “synthetically” and simplified to the point that it could be taught to undergraduates. After a brief tour the type theory we employ, we introduce ∞-categories and ∞-groupoids and explore the relationship between these notions.
Joint work with Michael Shulman.
10:00 – 10:30
John Harding, New Mexico State University

Decompositions in quantum mechanics

This is an approach to the foundations of quantum mechanics that takes focus from the structure of Hilbert spaces and places it on what one does with Hilbert spaces. For nearly any type of structure, such as a set or topological space, its direct decompositions form an orthomodular poset that allows basic aspects of quantum mechanics. This includes treatment of experiments, observables, and dynamics. These ideas extend to to objects in any category with well-behaved finite products.
Further aspects of quantum mechanics require additional features on the structure. The existence of a norm allows development of states, probabilities of outcomes, and expected values of observables. The existence of a tensor, or monoidal structure, allows for composite systems. 
We give an overview of this topic. 
10:30 – 11:00 Coffee Break / Discussion
11:00 – 11:45

 Arthur Jaffe, Harvard University

A New Look at Pictures in Quantum Information

I review some recent work done with Zhengwei Liu and our collaborators.  It marks the start of what we believe is a fruitful approach to certain problems in quantum information.

11:45 – 12:15 Michael Mislove, Tulane University

Semantic Models of Quantum Programming Languages: Recursion in Linear / Nonlinear Models

This work focuses on defining semantic models for high level functional quantum programming languages that support recursion. The work was inspired by Rios’s and Selinger’s language Proto-Quipper-M, a finitary circuit description language for quantum programs, The models are based on Benton’s work on linear / nonlinear models for the lambda calculus, adding an enriched structure needed to define recursion. I’ll describe our constructions, and the issues that were the most challenging. Our models support recursive terms and recursive types, and we have soundness and computational adequacy under appropriate hypotheses. Since the focus is on circuit description languages, there is no notion of an execution of a quantum programs. For that, we need to add dynamic lifting, so that measurements are included in the models. That remains future work.

Joint work with Bert Lindenhovius and Vladimir Zamdzhiev

12:15 – 1:15 Lunch / Discussion
1:15 – 1:45 Shawn Xingshan Cui, Virginia Polytechnic Institute and State University

On topological quantum computing

Topological quantum computing (TQC) is among the best approaches to building a large-scale fault-tolerant quantum computer. The quantum media for TQC are topological phases of matter that harbor non-Abelian anyons and quantum gates are implemented by braiding of anyons. The mathematics of topological phases of matter is described by modular tensor categories or equivalently by topological quantum field theories. We give a review on the rich interactions between TQC and the subjects mentioned above. We illustrate the concept of TQC with an important class of anyons, namely, metaplectic anyons, and show that braidings of anyons assisted by certain topologically protected measurements is universal for quantum computing. The interest in metaplectic anyons arises from the potential physical realization in fractional quantum Hall systems. Time permitting, we also talk about the application of topological quantum field theories in topology and give a new invariant of smooth 4-manifolds of state-sum type. 

1:45 – 2:15 Zhenghan Wang, UCSB
Is the quantum model of computation unique? 

The circuit model of quantum computing is based on quantum mechanics. If there would be a unique quantum model of computation, then quantum field theories can be efficiently simulated by quantum computers. I will discuss a program to efficiently simulate (1+1)-conformal field theories based on anyonic chains and insights gained from the efficient quantum simulation of TQFTs using the higher category language. The talk is based on the joint work with Shokrian Zini.

2:15 – 3:00 Louis H Kauffman, University of Illinois at Chicago

Topological Computing, Knots, Braids and Higher Categories

This talk will review relationships between knots, braids and topological computing with an eye towards relationships with categories and higher categories. We will review anyonic topological computing — the Fibonacci model and braiding representations using Majorana Fermions. We will discuss how categories are related to knot invariants and to the categorification of knot invariants and how one can, in principle, write quantum algorithms for categorified invariants such as Khovanov homology. The relationships with higher categories that we discuss are those directly related to knot diagrams, to categorifications and to higher dimensional knots such as embedded surfaces in four dimensional space and braiding of anyons represented by closed loops and knots.

3:00 – 3:30 Coffee Break / Discussion
3:30 – 4:00 Jacek Jakowski, ORNL

Quantum chemistry benchmark for quantum computing

We present a quantum chemistry benchmark for noisy intermediate-scale quantum computers. The proposed benchmark includes alkali metal hydrides with various basis sets and leverages variational eigensolver, various error mitigation strategies and XACC (eXtreme-scale ACCelerator) software framework. XACC follows a coprocessor machine model that is independent of the underlying quantum computing hardware, thereby enabling quantum programs to be defined and executed on a variety of QPUs types through a unified application programming interface. Our results provide a relevant baseline for future improvement of the underlying hardware.

4:00 – 4:30 Paul Gustafson, AFRL

Dimension as a quantum statistic and applications

We discuss several useful interpretations of the categorical dimension of objects in a braided fusion category, as well as some conjectures demonstrating the value of quantum dimension as a quantum statistic for detecting certain behaviors of anyons in topological phases of matter. From this discussion we find that objects in braided fusion categories with integral squared dimension have distinctive properties.  We illustrate these ideas in the case of metaplectic modular categories. This is joint work with Eric Rowell and Yuze Ruan.

4:30 – 5:00 Carl Alexander Miller, University of Maryland, College Park
Picture-proofs for quantum cryptography based on categorical quantum mechanics 

Formal visual reasoning in quantum information not only makes some proofs clearer, but also enables new proofs that would have otherwise been very difficult.  In the current work we start with a known visual language (from categorical quantum mechanics) and add new features to it in order to make a language that is amenable to quantum cryptography. We give a diagrammatic proof of a new result (parallel self-testing of the GHZ state) and also re-prove a known result (linear randomness expansion implies unbounded randomness expansion).  We computer-verify the main sequence of the second proof using the Globular software package.  This is joint work with Spencer Breiner, Neil J. Ross, and Amir Kalev.

5:00 – 5:30 Robert Rand, University of Maryland

Formally Verifying Quantum Protocols

This talk presents QWIRE, a tool for writing quantum programs and proving them correct. QWIRE allows us to describe quantum circuits and translate those circuits into functions on quantum states, whether represented as unit vectors or density matrices. We can then prove that these functions behave as desired, using a variety of reasoning techniques. We discuss existing approaches to verifying quantum algorithms using QWIRE as well as ongoing work to verify error-prone quantum computations.

5:30 – 6:00 Omar Shehab, IonQ

Verification and certification of noisy intermediate-scale quantum computing

In this talk I briefly introduce the concept of noisy intermediate-scale quantum computing. Then I demonstrate a toy nuclear physics problem we solved on a trapped ion quantum computer with reasonable accuracy. Finally, I discuss the potential ways one would verify and certify the outcome of this computation.

6:00 Dinner / Discussion