Quantum computing hardware has made significant progress in the past decade. Great efforts are devoted to designing quantum programming languages to solve real-world problems using quantum computers. Composing correct quantum programs is difficult due to the counter-intuitive nature of quantum mechanics. To verify the correctness of quantum programs, we propose two approaches of quantum assertions: 1. Tomography-based assertions; 2. Birkhoff & von Neumann's quantum logic. In the first part of this talk, I will relate the implementation cost of tomography-based assertions and review our work which closes a 40 years' long-standing gap between the upper and lower bounds for quantum state engineering. In the second part of this talk, I will overview our work of applied quantum Hoare logic and quantum abstract interpretation that leverage the power of Birkhoff & von Neumann's quantum logic in efficient reasoning about quantum programs. I will conclude my talk with opportunities and challenges.
Nengkun Yu is a Senior Lecturer in the Centre for Quantum Software and Information, University of Technology Sydney. He received the B.S. and Ph.D. degrees from the Department of Computer Science and Technology, Tsinghua University, Beijing, China, in July of 2008 and 2013, respectively. From January 2014 to July 2016, he was a postdoc at the Institute for Quantum Computing at the University of Waterloo, Canada. He won the J G Russell Award from the Australian Academy of Science in 2018, and an ACM SIGPLAN distinguished paper award at OOPSLA 2020. His research interest focuses on quantum computing.
Faculty host: Vikram Adve