A Unified Assertion-Based Framework for Classical-Quantum Program Verification (PLanQC 2026) - POPL 2026

Sun 11 - Sat 17 January 2026 Rennes, France

Track

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Mon 12 Jan 2026 14:30 - 14:50 at Salle 14 - Session 3

Abstract

We point out several interleaved challenges for formal verification of practical quantum programs and propose a new framework that is intuitive, easy to use, and works well with interactive theorem provers. The key insights are classicality by subtype and assertion-based predicates and Hoare logic.

File attachments

Extended Abstract (planqc26-paper7.pdf)	548KiB

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

	13:50 - 15:30	Session 3PLanQC at Salle 14

	13:50 20m Talk		A Graded Modal Type Theory for Pulse SchedulesTalk PLanQC Robin Adams Chalmers University of Technology, Gothenburg University, Sweden, Jean-Philippe Bernardy Chalmers University of Technology, Gothenburg University, Sweden, Lorenzo Perticone Chalmers University of Technology, Gothenburg University, Sweden, Jeremy Pope Chalmers University of Technology, Gothenburg University, Sweden File Attached
	14:10 20m Talk		Efficient Parallel Compilation and Profiling of Quantum Circuits at Large ScalesTalk PLanQC Jane Moore Queen's University Belfast, Michael Hart Queen's University Belfast, John McAllister Queen's University Belfast File Attached
	14:30 20m Talk		A Unified Assertion-Based Framework for Classical-Quantum Program VerificationTalk PLanQC Yingte Xu File Attached
	14:50 20m Talk		A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and EmulationRemote PLanQC Yu-Hsuan Wu Academia Sinica, Yue Shi Princeton University, Junyi Liu University of Maryland, Yuxiang Peng Purdue University File Attached
	15:10 20m Talk		Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies and Lower BoundsRemote PLanQC Shengyuan Yang University of Wisconsin-Madison, Charles Yuan University of Wisconsin–Madison File Attached

Hide past events

Yingte Xu