Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
Fri 17 Jun 2022 04:10 - 04:30 at Toucan - Quantum
We investigate the \emph{algebraic} reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative, and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum \textbf{while}-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50 | |||
15:30 20mTalk | Quartz: Superoptimization of Quantum Circuits PLDI Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University DOI | ||
15:50 20mTalk | Giallar: Push-button Verification for the Qiskit Quantum Compiler PLDI Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University DOI | ||
16:10 20mTalk | Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra PLDI Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD DOI | ||
16:30 20mTalk | PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics PLDI Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara DOI |
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
03:30 - 04:50 | |||
03:30 20mTalk | Quartz: Superoptimization of Quantum Circuits PLDI Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University DOI | ||
03:50 20mTalk | Giallar: Push-button Verification for the Qiskit Quantum Compiler PLDI Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University DOI | ||
04:10 20mTalk | Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra PLDI Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD DOI | ||
04:30 20mTalk | PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics PLDI Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara DOI |