A Rewriting Theory for Quantum Lambda-Calculus
Claudia Faggian, Gaetan Lopez, Beno\^it Valiron

TL;DR
This paper develops a rewriting theory for quantum lambda calculus, focusing on standardization and normalization, leveraging recent advances in probabilistic rewriting to address gaps in the theoretical understanding of quantum programming languages.
Contribution
It introduces a rewriting framework for quantum lambda calculus, providing foundational results on standardization and normalization that were previously lacking.
Findings
Established a formal rewriting theory for quantum lambda calculus.
Proved standardization and normalization theorems within this framework.
Utilized recent probabilistic rewriting techniques to advance quantum programming language theory.
Abstract
Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
