On Coinduction and Quantum Lambda Calculi
Yuxin Deng, Yuan Feng, and Ugo Dal Lago
In the ubiquitous presence of linear resources in quantum computation, program equivalence
in linear contexts, where programs are used or executed once, is more important than in
the classical setting. We introduce a linear contextual equivalence and two notions of
bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning
about higher-order quantum programs. Both notions of bisimilarity are sound with respect to
the linear contextual equivalence, but only the distribution-based one turns out to be
complete. The completeness proof relies on a characterisation of the bisimilarity as
a testing equivalence.