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 λ-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.
Applicative bisimulation and quantum λ-calculi / Dal Lago, Ugo; Rioli, Alessandro. - ELETTRONICO. - 9392:(2015), pp. 54-68. (Intervento presentato al convegno 6th International Conference on Fundamentals of Software Engineering, FSEN 2015 tenutosi a Iran nel 2015) [10.1007/978-3-319-24644-4_4].
Applicative bisimulation and quantum λ-calculi
DAL LAGO, UGO;RIOLI, ALESSANDRO
2015
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 λ-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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
