PLanQC 2022
as the organisers put it
The Third International Workshop on Programming Languages for Quantum Computing (PLanQC 2022) 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
programming languages researchers, quantum information researchers, formal verification researchers, type system researchers, compiler engineers, quantum software engineers
topics
topological quantum programming; python-embedded quantum language; purity and entanglement types; circuit-to-Hamiltonian embedding; quantum separation logic in F*; qutrit Clifford+T compilation; synthesis into fixed XX interactions; encoding programs as SZX-diagrams; type-safe variational programming in Idris; quantum relational Hoare logic; reversible data structures in superposition
| title | author | length |
|---|---|---|
| Topological Quantum Programming in TED-K | Hisham Sati, Urs Schreiber | 22m |
Describes a concrete programming scheme that encodes SU(2) anyon wavefunctions (Majorana/Ising and Fibonacci) as twisted equivariant differential K-cohomology… | ||
| Qrisp: A Framework for Compilable High-Level Programming of Gate-Based Quantu... | Raphael Seidel, Sebastian Bock, Nikolay Tcholtchev, Manfred Hauswirth | 26m |
Qrisp is a Python-embedded high-level language that actually compiles down to gate-level circuits and runs on simulated IBM and Quantinuum backends via a… | ||
| Invited talk: Twist: Sound Reasoning for Purity and Entanglement in Quantum P... | Charles Yuan | 44m |
Twist is a quantum language that encodes a type system for purity so programs can assert lack of entanglement and have those assertions checked by a mix of… | ||
| Analyzing quantum programs using the power of interaction | Agnes Villanyi, Charles Yuan, Christopher McNally | 21m |
Proposes two concrete verification routes: embed execution into a circuit-to-Hamiltonian embedding so the correct run is the ground-state witness and avoid… | ||
| Q*: Implementing Quantum Separation Logic in F* | Kesha Hietala, Sarah Marshall, Robert Rand, Nikhil Swamy | 16m |
Prototype implements quantum separation logic inside F using the Steel library and Z3 for automation, ports Quantum Lib, and adds four quantum actions… | ||
| Adventures in Qutrit Compilation | Lia Yeh, John van de Wetering | 24m |
Gives an explicit, ancilla-free construction for any qutrit multiple-controlled Toffoli and shows any Clifford+T qutrit unitary can have arbitrarily many… | ||
| Optimal synthesis into fixed XX interactions | Eric C. Peterson, Lev S. Bishop, Ali Javadi-Abhari | 24m |
An optimal, efficient procedure and software implementation compiles any 4x4 unitary into a discrete set of XX interactions and returns exact or approximate… | ||
| Encoding High-level Quantum Programs as SZX-diagrams | Agustín Borgna, Rafael Romero | 17m |
Method encodes a bounded fragment of Proto-Quipper-D into Scalable ZX-diagram families by translating type judgments into diagram templates; vectors become… | ||
| Type-safe (Variational) Quantum Programming in Idris | Liliane-Joy Dandy, Emmanuel Jeandel, Vladimir Zamdzhiev | 18m |
Qimaera implements variational quantum programming as Idris 2 libraries that use dependent types and linearity to guarantee at compile time that circuits… | ||
| Quantum relational Hoare logic, towards a formalization | Dominique Unruh | 35m |
Quantum relational Hoare logic (qRHL) formalizes relationships between two quantum programs by interpreting pre/postconditions as subspaces of joint memory and… | ||
| Tower: Data Structures in Quantum Superposition | Charles Yuan, Michael Carbin | 26m |
Implements a language and runtime that realize reversible, history‑independent, bounded‑time data structures for quantum algorithms: Tower provides reversible… | ||
| nothing matches | ||