A feasible and unitary quantum programming language
Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux, Mário Silva
TL;DR
PUNQ introduces a higher-order quantum programming language with quantum control that guarantees both unitarity and polynomial-time normalization. By intertwining a DLAL-inspired polytime type discipline with a Lambda-$\mathcal{S}_1$-style unitarity framework, the language enforces linear use of qubits, orthogonality of superpositions, and controlled duplication to satisfy the no-cloning theorem, while ensuring that all typable programs normalize in polynomial time and produce polynomial-size outputs. Core results include subject reduction, progress, realizability-based unitarity, completeness for isometries, and a PTIME-type-checking landscape across orthogonality-fragmented sublanguages; Grover, teleportation, and quantum-walk examples illustrate practical feasibility. The work advances quantum programming by delivering a single, coherent framework that combines higher-order quantum control with rigorous resource and complexity guarantees, potentially enabling reliable compilation to quantum circuits within practical bounds.
Abstract
We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality forsuperpositions while requiring orthogonality among superposed terms. Polynomial-time normalization isachieved using a linear-logic-based type discipline employing Barber and Plotkin duality along with a specificmodality to account for potential duplications. This type discipline also guarantees that derived values havepolynomial size. Our language seamlessly combines the two modalities: quantum circuit programs upholdunitarity, and all programs are evaluated in polynomial time, ensuring their feasibility.