PLanQC 2025
as the organisers put it
The Fifth International Workshop on Programming Languages for Quantum Computing (PLanQC 2025) aims to bring together researchers from the fields of programming languages and quantum information, 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. Workshop topics include (but are not limited to): High-level quantum programming languages Verification tools for q ...
who it's for
quantum programming language researchers, quantum compiler engineers, quantum software engineers, formal methods and verification researchers, quantum tool and infrastructure builders, quantum algorithm developers, programming languages researchers
topics
reversible and controllable circuits; Proto-Quipper extensions; quantum abstract machine semantics; projective Clifford lambda calculus; ownership and borrowing for qubits; fuzzing quantum compilers; algebraic IO semantics for quantum; chiplet-aware compiler partitioning; automata-based circuit verification; quantum register machine and QRAM; graph-based quantum-classical IR (HUGR); quantum multiparty session types
| title | author | length |
|---|---|---|
| Proto-Quipper with Reversing and Control | Peng Fu, Kohei Kishida, Neil Julien Ross, Peter Selinger | 20m |
Formalizes reversible and controllable circuits with a dagger symmetric monoidal category R and a new controllable category N, adds a Proto-Quipper extension… | ||
| The Quantum Abstract Machine | Le Chang, Liyi Li, Rance Cleaveland, Mingwei Zhu, Xiaodi Wu | 19m |
Defines a Quantum Abstract Machine that gives direct semantics to circuit primitives (teleportation, entanglement swap) using a Chemical Abstract Machine… | ||
| Programming with Projective Cliffords | Jennifer Paykin, Sam Winnick | 24m |
Defines a lambda calculus LambdaPC whose well‑typed functions are exactly projective Cliffords acting by conjugation on the Pauli group, proves a Curry-Howard… | ||
| Imperative Quantum Programming with Ownership and Borrowing in Guppy | Mark Koch, Agustín Borgna, Craig Roy, Alan Lawrence, Kartik Singhal, Seyon Sivarajah, Ross Duncan | 24m |
Guppy implements an imperative quantum type system that enforces ownership and borrowing so you cannot measure or deallocate a qubit you don’t own, borrows… | ||
| QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control(…) | Ilan Iwumbwe, Benny Zong Liu, John Wickerson | 16m |
QuteFuzz generates fully random quantum programs with nested subroutines and control flow, runs them through Qiskit, Pytket and Cirq stacks, and does… | ||
| Algebraic and denotational semantics for Classically Controlled Quantum Communication | Theo Wang, Sam Staton | 22m |
Claims a parameterised algebraic theory for classically controlled quantum I/O and gives two sound models: a quantum stream operational semantics (streams as… | ||
| Unlocking quantum potential with software and compilers | Kaitlin Smith | 46m |
Describes compiling algorithms into hardware-ready circuits, showing that devices reach ~1,000 qubits today but require millions for fault tolerance, so… | ||
| An Automata-based Framework for Quantum Circuit Verification | Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Kai-Min Chung, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai, Di-De Yen | 22m |
Framework encodes sets of quantum basis trees as tree automata (BDD-like tries) and implements gate updates symbolically — X swaps left/right branches, S… | ||
| Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs(…) | Zhicheng Zhang, Mingsheng Ying | 21m |
Proposes a quantum register machine architecture with a 22-instruction set and a quantum program counter, compiles RQ++ into low-level Qins, and uses a QF… | ||
| HUGR: A Quantum-Classical Intermediate Representation | Seyon Sivarajah, Mark Koch, Agustín Borgna, Alan Lawrence, Alec Edgington, Douglas Wilson, Craig Roy, Luca Mondada, Lukas Heidemann, Ross Duncan | 23m |
HUGR is a graph‑based intermediate representation that encodes mixed quantum‑classical programs with strict, static typing and linear quantum types to prevent… | ||
| Towards Quantum Multiparty Session Types | Ivan Lanese, Ugo Dal Lago, Vikraman Choudhury | 24m |
Proposes Quantum MPSTs that extend multiparty session types with linearity and quantum primitives, implements an operational semantics as a labeled transition… | ||
| Verifying the Equivalence of Parameterized Quantum Circuits | Scott Wesley, Neil Julien Ross | 22m |
Claims that parameterized-circuit equivalence reduces to checking Laurent polynomial identities and gives concrete degree bounds computed from a circuit's… | ||
| Concurrent Quantum Separation Logic for Fine-Grained Parallelism | Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka | 24m |
A new concurrent quantum separation logic claims modular verification of fine‑grained parallel quantum code by combining three concrete mechanisms: fractional… | ||
| nothing matches | ||