Basis-Sensitive Quantum Typing via Realisability

TL;DR

This paper introduces a basis-sensitive quantum lambda calculus with a realisability semantics, enabling precise reasoning about quantum programs under basis changes and ensuring type safety.

Contribution

It extends previous quantum lambda calculi by allowing abstractions with respect to arbitrary bases, including entangled ones, and provides a semantics-based foundation for a type-safe quantum programming language.

Findings

Successfully models quantum algorithms like Deutsch's algorithm and teleportation.

Ensures safety and correctness through a basis-dependent type system.

Provides a semantics that characterizes unitary operators and program behavior.

Abstract

We present $\lambda_B$, a quantum-control $\lambda$-calculus that refines previous basis-sensitive systems by allowing abstractions to be expressed with respect to arbitrary -- possibly entangled -- bases. Each abstraction and let construct is annotated with a basis, and a new basis-dependent substitution governs the decomposition of value distributions. These extensions preserve the expressive power of earlier calculi while enabling finer reasoning about programs under basis changes. A realisability semantics connects the reduction system with the type system, yielding a direct characterisation of unitary operators and ensuring safety by construction. From this semantics we derive a validated family of typing rules, forming the foundation of a type-safe quantum programming language. We illustrate the expressive benefits of $\lambda_B$ through examples such as Deutsch's algorithm and quantum teleportation, where basis-aware typing captures classical determinism and deferred-measurement behaviour within a uniform framework.