Quantum Compiler Co-Created by Robert Rand Named Distinguished Paper at POPL 21

If programmers want to use quantum computers today or in the near future, they’re going to have to get the most out of small, error-prone machines. Fortunately, they have a helpful tool at hand: the compiler. The translators of the programming stack, compilers convert human-readable code to the explicit instructions that computing machinery, classical or quantum, need to operate. Some can even improve that code along the way, making it faster and more reliable.

A new compiler that does all of the above for today’s early quantum computers received one of seven Distinguished Paper awards this month at the 2021 Symposium on Principles of Programming Languages (POPL), one of the top conferences in programming languages research. VOQC, developed by UChicago CS assistant professor Robert Rand and collaborators at the University of Maryland, is the first verified quantum optimizer — a tool for rewriting programs to make them faster while guaranteeing that the program’s meaning is preserved. 

The ecosystem of quantum compilers is still small, and new arrivals can produce a large impact in this young field. The ability of VOQC to not only get the most out of the current generation of quantum computers but also prevent errors provides a huge boost to programmers working in an exciting new paradigm.

“We need an optimizing compiler for quantum computing because the hardware is in its infancy. It is incredibly limited, and we need to take advantage of literally every single qubit on the hardware,” Rand said. “Furthermore, these machines are incredibly error-prone, and quantum programs are very difficult to write. So whenever we plug a potential source of error, it’s a big step towards being able to write and execute correct programs and pinpoint the source of programmer or machine errors.”

VOQC, pronounced “vox,” gains its unique abilities through the use of formal verification, methods that convert a computer program or algorithm to a mathematical proof in order to rigorously confirm that its outputs are correct. The project was inspired by CompCert, a verified compiler built for the C language that used the Coq proof assistant to optimize code and prevent bugs. But formal verification could be even more critical for quantum computing, where the underlying physics of the hardware and the possibility of applications that can’t be performed or confirmed on a classical computer create additional uncertainty.

To help VOQC work its magic, Rand and his team developed a quantum intermediate language called SQIR (“squire”). Programmers can write code in a high-level quantum programming language — including QWIRE, a mathematically-grounded language co-developed by Rand — and then convert their program to SQIR, a language closer to the actual instructions for the quantum hardware. With UChicagoCS PhD student Kartik Singhal, Rand is currently working on a verified SQIR translator for IBM’s OpenQASM standard, and hope to build similar tools for popular quantum languages like Q# and Silq.

These projects are part of Rand’s overall goal of building up the quantum programming stack and installing formal verification at every step of the process. While CompCert only appeared after decades of C programming, VOQC arrives in the early days of quantum computing, with the potential to help shape the field as it grows. Given the unreliability of today’s hardware and the inherent complexities of quantum physics and computing, the extra layer of validation will help the field move past its awkward stage as quickly as possible and move on to unprecedented feats of computation.

“In general, what we want to do is set a high standard for quantum programming languages and quantum computing,” Rand said. “We want to apply lessons from decades of classical computing research right at the beginning, and compilers were a major success story case for formal verification.”

The paper, “A Verified Optimizer for Quantum Circuits,” was presented online at POPL 21 on January 20th. In addition to Rand, co-authors include Kesha Hietala, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, all of University of Maryland. For more on the project and the award, see the University of Maryland news article. You can also watch the POPL 21 talk and Q&A here.

[Image: “IBM 7 Qubit Device” by IBM Research is licensed with CC BY-ND 2.0.]

Related News

More UChicago CS stories from this research area.
UChicago CS News

UChicago London Colloquium Features Data Science, Quantum Research

Jul 01, 2022
UChicago CS News

EPiQC Post-Doc Pens Op-Ed on Potential of Quantum Computing for Chemistry

Jun 24, 2022
UChicago CS News

Faculty Bill Fefferman and Chenhao Tan Receive Google Research Scholar Awards

Jun 21, 2022
UChicago CS News

UChicago CS Spinout Super.tech Acquired by Quantum Ecosystem Leader ColdQuanta

May 10, 2022
UChicago CS News

First-Year PhD Student Co-Authors Outstanding Paper Award Winner at TQC 2022

Apr 28, 2022
UChicago CS News

Super.tech/EPiQC Quantum Computing Benchmark Receives Best Paper Award

Apr 14, 2022
UChicago CS News

Concurrency Bug Research by Prof. Shan Lu Receives ASPLOS Influential Paper Award

Mar 29, 2022
In the News

Quanta Magazine Features Prof. Bill Fefferman’s Work on Quantum Algorithms

Jan 20, 2022
UChicago CS News

In-Fridge Controller Could Scale Up Quantum Computers, Award-Winning UChicago Research Finds

Jan 10, 2022
UChicago CS News

EPiQC Research Receives Best Paper Award at IEEE Quantum Week

Oct 22, 2021
UChicago CS News

UChicago and EPiQC Alum Yongshan Ding Joins Yale in Faculty Position

Oct 08, 2021
UChicago CS News

Five UChicago CS Students Named to Siebel Scholars 2022 Class

Sep 23, 2021
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube