Speaker: Yuxin Deng
Title: On Coinduction and Quantum Lambda Calculi
Abstract: 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.