Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
Bichsel and colleagues introduce Silq, using type annotations for safe automatic uncomputation and simpler quantum-program semantics.
Paper information (2020, PLDI) — Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. DOI; author page
Work
Silq addresses the need to explicitly uncompute temporary values in high-level quantum languages by providing safe automatic uncomputation. It permits temporary values to be dropped implicitly, as in classical programs, while type annotations reject programs whose semantics would be physically invalid. The paper reports shorter Silq programs and fewer quantum primitives than selected Q# and Quipper equivalents.
Contributions
- A high-level quantum language with safe automatic uncomputation.
- Type-system annotations that preserve physical realizability of the semantics.
- Intuitive semantics for implicitly dropping temporary values.
- Experimental comparisons of program length and quantum-primitive counts.
Limits
Safety depends on the type system, semantics, and compiler implementation; shorter source code does not imply faster or more reliable circuits on every backend. The experiments cover selected programs and languages and do not automatically generalize to all algorithms, noise models, gate sets, or full formal proofs.
Connections
Silq continues the typed high-level-language line of QPL and the quantum lambda calculus, and offers a language-engineering comparison with Quipper. Its automatic-uncomputation problem also connects to the resource-use constraints of Linear Type Systems.
Original paper
Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev, Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics, in PLDI 2020, DOI: 10.1145/3385412.3386007. Author page