A Rewriting Theory for Quantum λ-Calculus

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 are standardization and normalization results.

Authors

• Claudia Faggian
• Gaetan Lopez
• Benoît Valiron

Keywords

• quantum lambda-calculus
• probabilistic rewriting
• operational semantics
• asymptotic normalization
• principles of quantum programming languages