PLanQC 2026
as the organisers put it
The Sixth International Workshop on Programming Languages for Quantum Computing (PLanQC 2026) aims to bring together researchers from the fields of programming languages and quantum information science, exposing the programming languages community to the unique challenges of programming quantum computers. It will promote the development of tools to assist in the process of programming quantum computers, both those that exist today and those likely to exist in the near to far future. Topics of particular interest include: High-level quantum programming languages Verification tools for quan ...
who it's for
quantum programming languages researchers, quantum compiler developers, formal verification researchers, quantum control engineers, quantum algorithm designers, quantum software engineers, quantum hardware engineers
topics
pulse-level DSL with RISC-V binaries; real-time RFSoC emulation; graded modal type theory for schedules; operator-space von Neumann models; hierarchical circuit language with control product; Repeat-Until-Success circuit verification; block-encoding quantum linear algebra; path-sum symbolic verification; query-count cost model for classical-to-quantum; denotational stabiliser semantics; assertion-based classicality by subtype; quantum assertion testing without mid-circuit measurement
| title | author | length |
|---|---|---|
| Opening Address | Vladimir Zamdzhiev | 06m |
Schedule changes force a shorter lunch by 10 minutes less lunch so the program fits two extra talks; the keynote Christo Charton at 11:00 is expected by train… | ||
| A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and Emulation | Yu-Hsuan Wu, Yue Shi, Junyi Liu, Yuxiang Peng | 18m |
A pulse-level DSL, compiler, and emulator stack provides deterministic real-time quantum control by compiling programs to RISC‑V binaries that run on… | ||
| A Graded Modal Type Theory for Pulse Schedules | Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, Jeremy Pope | 20m |
Provides a pair of linearly typed languages with semantics in symmetric monoidal categories: a plain circuit language and Grampus, an annotated language that… | ||
| Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach | Thea Li, Vladimir Zamdzhiev | 22m |
Presents a concrete categorical model of MALL built inside finite-dimensional operator spaces and finite-dimensional von Neumann (co)algebras, using the… | ||
| Towards a Hierarchical Quantum Circuit Language | William Schober, Scott Wesley | 20m |
Introduces a hierarchical circuit language that adds two concrete connectives: subcircuit exponentiation (matrix power via log/exp) and a novel control product… | ||
| Verifying Repeat-Until-Success Circuits with AutoQ | Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlik, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai | 17m |
A new characterization theorem pins exactly which two‑qubit Repeat‑Until‑Success (RUS) circuits implement single‑qubit unitaries, and AutoQ is extended into an… | ||
| Programming Abstractions for Quantum Linear Algebra | Charles Yuan | 22m |
Cobble is a domain language that compiles algebraic matrix expressions into circuits operating on block encodings, tracking both query count and the crucial… | ||
| Democratizing quantum formal verification: the path-sum way | Christophe Chareton | 40m |
A verification tool called Cubri uses the path-sum symbolic execution format to represent quantum states as phased sums, claims compact proofs for many… | ||
| One rig to control them all | Chris Heunen, Robin Kaarsgaard, Louis Lemonnier | 23m |
A synthetic construction adds eight equations to any base prop of gates to produce controlled gates and their iterated controls, and the paper proves this… | ||
| Traq: Estimating the Quantum Cost of Classical Programs | Anurudh Peduri, Jam Kabeer Ali Khan, Gilles Barthe, Michael Walter | 19m |
Traq provides an automated pipeline that compiles a classical CPL source language to unitary quantum code, extracts three cost functions (worst-case have cost… | ||
| Denotational semantics for stabiliser quantum programs | Robert I. Booth, Cole Comfort | 14m |
Claims a sound, universal and complete denotational semantics for stabiliser operations that includes measurement, classical control and quantum… | ||
| A Unified Assertion-Based Framework for Classical-Quantum Program Verification | Yingte Xu | 23m |
Proposes an assertion-based verification framework that marks classical registers by classicality by subtype so all variables remain quantum but some satisfy… | ||
| Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies and Lower Bounds | Shengyuan Yang, Charles Yuan | 20m |
Defines FirstFail and exist-fail tasks and proves concrete time‑space limits: any strategy without mid‑circuit measurement satisfies T × S = Ω(log n). Provides… | ||
| nothing matches | ||