Professor Mingsheng Ying
LECTURE SERIES · QUANTUM SOFTWARE & VERIFICATION

Foundations of
Quantum Programming

Distinguished Professor Mingsheng Ying
University of Technology Sydney
28 September – 2 October 2026 DATE
10:00 – 12:00 JST TIME
W1-C-502 ROOM
Kyushu University · Ito Campus VENUE
01

Lecturer

Professor Mingsheng Ying is internationally recognised for his contributions to quantum computing, quantum programming, and quantum software verification. He is a Distinguished Professor at the UTS Centre for Quantum Software and Information at the University of Technology Sydney.

His research interests include quantum computation, programming language theory, quantum program semantics, verification, and the foundations of quantum software.

Professor Ying is Co-Editor-in-Chief of ACM Transactions on Quantum Computing and has served in editorial roles for several leading journals and conferences.

02

Abstract

Recent advances in quantum hardware have brought the field from prototype devices to increasingly practical platforms.

To fully realise the potential of quantum computing, quantum programming and software-development technologies will play a crucial role.

This lecture series systematically introduces the theoretical foundations of quantum programming, including operational and denotational semantics, quantum program logics with an emphasis on quantum Hoare logic, verification and analysis of quantum programs, and quantum recursive programming.

The lectures will also discuss open problems that may inspire future research in quantum programming.

03

Main Topics

  1. Operational semantics of quantum programs
  2. Denotational semantics of quantum programs
  3. Quantum Hoare logic
  4. Verification and analysis of quantum programs
  5. Quantum recursive programming
  6. Open problems and future research
04

Recent Research

[1]M. S. Ying, A Practical Quantum Hoare Logic with Classical Variables, Information and Computation, 2026.
[2]M. S. Ying, L. Zhou, and G. Barthe, Laws of Quantum Programming, ACM Transactions on Software Engineering and Methodology, 2026.
[3]M. S. Ying and Z. C. Zhang, Verification of Recursively Defined Quantum Circuits, Proceedings of PLDI, 2026.
05

Recommended Book

2nd Edition · Elsevier · 2024

Foundations of Quantum Programming

by Mingsheng Ying

This book provides a comprehensive introduction to the theory and practice of quantum programming, covering quantum computational models, programming languages, program semantics, and formal techniques for reasoning about quantum software.

The book explains how concepts from classical programming can be extended to the quantum setting while addressing the distinctive challenges of quantum computation.

The second edition adds new material on parallel and distributed quantum programming, quantum machine learning, and advanced techniques for analysing and verifying quantum programs.

Cover of Foundations of Quantum Programming, 2nd Edition
06

Mini-Workshop & Contributed Talks

Engaging the next generation of quantum-programming researchers

The intensive lecture series will be complemented by a mini-workshop designed to actively engage participants, especially students and early-career researchers. Attendees will have the opportunity to give short contributed talks on their research, ideas, or ongoing projects related to quantum programming, quantum software, formal methods, and verification.

The talks will provide a valuable opportunity to receive feedback and discuss research directions with Prof. Mingsheng Ying and invited speakers from Kyushu University and JAIST. The aim is to create an informal and constructive environment for exchanging ideas, identifying promising research problems, and developing future collaborations.

INVITED SPEAKERS

Canh Minh Do (Japan Advanced Institute of Science and Technology)

Masao Hirokawa (Faculty of Information Science and Electrical Engineering, Kyushu University)

Hiroyuki Ochiai (Institute of Mathematics for Industry, Kyushu University)

Jianjun Zhao (Faculty of Information Science and Electrical Engineering, Kyushu University)

Interested in giving a contributed talk? Participants who would like to present their work are encouraged to indicate their interest during registration. Alternatively, attendees may contact the organizer directly to express their intention to give a talk.

07

Why Attend?

  • Learn the mathematical foundations of quantum software
  • Understand modern quantum verification techniques
  • Explore current research challenges
  • Discover opportunities for graduate research
  • Interact with leading researchers in quantum programming
08

Event Information

LOCATION W1-C-502 Kyushu University, Ito Campus
DATE 28 September – 2 October 2026
TIME Lecture: 10:00 – 12:00 JST Workshop: 13:00 – 15:00 JST
09

Registration

Register for the lecture series

Participation is open to students, researchers, faculty members, and anyone interested in quantum programming and quantum software.

Please complete the registration form prior to attending. Participants are strongly encouraged to attend the event in person. However, the event will be available in a hybrid format. Those attending online will receive the Zoom link by email.

Open Registration Form ↗

You can also scan the QR code to open the registration form.

QR code for the registration form
10

Organizer

Daniel Gaina
daniel@imi.kyushu-u.ac.jp