PLanQC 2021
2021-06-22
-- online --
PLanQC ·
[PLanQC 2020, PLanQC 2021, PLanQC 2022, PLanQC 2024, PLanQC 2025, PLanQC 2026]
| title | author | length |
|---|---|---|
| Addressable quantum gates | Ulysse Rémond | 24m |
Introduces addressable quantum circuits: a circuit model that adds finite, consumable addresses as quantum data and alternates global scatter and transport… | ||
| Expanding the VOQC Toolkit | Kesha Hietala | 11m |
Vox is a Coq-verified quantum optimizer: every transformation has a formal proof of semantic preservation and some helper proofs (the U3 combination routine is… | ||
| Toward A Quantum Programming Language for Higher Level Formal Verification | Finn Voichick | 15m |
A new high-level language called quantum one targets formal verification by representing program state as superpositions of expressions and by encoding… | ||
| Reducing the CNOT count for Clifford+T circuits on NISQ architectures | Sarah Meng Li | 19m |
Presents a heuristic called slice and build that re-synthesizes Clifford+T circuits to cut CNOT count on connectivity-constrained NISQ graphs by combining… | ||
| Toward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem | Kartik Singhal | 17m |
Formal definition of Q# via a core calculus lambda qsharp models qubits as opaque symbols and surface qubits as qref references, introduces lifetime variables… | ||
| Quantum routing with fast reversals | Eddie Schoute | 18m |
A time‑independent XX+local field Hamiltonian implements state reversal on an n‑spin chain in time π/4·(n+1), versus swap‑based routing (swap time 3π/4) giving… | ||
| qKleene: Verification of Quantum RAM Made Easy | Roberto Giacobazzi | 16m |
qKleene is a small language that encodes control flow as regular-expression-like programs combining unbounded classical integers and bounded quantum registers… | ||
| Mitiq: A Python toolkit for quantum error mitigation | Andrea Mari | 19m |
A Python library called mitiq implements practical quantum error mitigation: zero-noise extrapolation and probabilistic error cancellation, plus… | ||
| JKQ: JKU Tools for Quantum Computing | Robert Wille | 20m |
JKU provides a toolkit that integrates with Qiskit and claims real gains by using decision diagrams for matrix and state compression; the simulator ddsim runs… | ||
| Theory, Design, and Implementation of Projection-based Assertions for Quantum Debugging | Yufei Ding | 32m |
Presents a concrete runtime testing method that inserts projection-based assertions as projective measurements, implements them on real gate-model devices by… | ||
| Quantum compilation using the ZX calculus | John van de Wetering | 31m |
ZX calculus is a graphical compiler backend that uses concrete rewrites—spider fusion, local complementation and pivot—to transform circuits into graph-like… | ||
| From Verified Compilation to Shor's Algorithm | Michael Hicks | 33m |
A verified compiler stack implements a small IR called Squire and a proven optimizer Vox that preserves denotational semantics across rewrites. The project… | ||
| Extending Gottesman Types Beyond the Clifford Group | Robert Rand | 16m |
Extends Gottesman-style types from Clifford-only to universal circuits by adding intersection types plus numeric additive types so T and arbitrary 1‑qubit… | ||
| Open Quantum Assembly Language | Steven Heidel | 16m |
A new OpenQASM version claims to add real-time classical control and pulse-level hardware control while remaining backwards compatible with OpenQASM2 programs… | ||
| Quantum and classical registers | Dominique Unruh | 17m |
Defines a register as a linear map that lifts any operator on a register Hilbert space to an operator on the whole memory, and requires it to be linear… | ||
| nothing matches | ||