Applicative Bisimulation and Quantum $\lambda$-Calculi (Long Version)

TL;DR

This paper extends applicative bisimulation to quantum lambda-calculi with probabilistic and quantum features, proving its soundness in this complex setting.

Contribution

It demonstrates that applicative bisimulation remains sound when applied to linear quantum lambda-calculi with probabilistic choice.

Findings

Applicative bisimulation is sound for quantum lambda-calculi.

Extension of bisimulation to probabilistic and quantum data.

Validation of bisimulation's applicability in quantum programming languages.

Abstract

Applicative bisimulation is a coinductive technique to check program equivalence in higher-order functional languages. It is known to be sound, and sometimes complete, with respect to context equivalence. In this paper we show that applicative bisimulation also works when the underlying language of programs takes the form of a linear $\lambda$-calculus extended with features such as probabilistic binary choice, but also quantum data, the latter being a setting in which linearity plays a role. The main results are proofs of soundness for the obtained notions of bisimilarity.