POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This paper presents a quantum extension of lambda calculus without linearity, reinterpreting contraction and weakening as logical operations on references to quantum states, rather than on the states themselves. We formally define the calculus with its operational semantics and conjecture that $\beta$-equal classical terms are contextually equivalent. This design enables the seamless integration of classical and quantum programming.

Extended Abstract (planqc26-paper9.pdf)524KiB