%0 Conference Proceedings
%T Applicative Bisimulation and Quantum λ-Calculi
%+ Foundations of Component-based Ubiquitous Systems (FOCUS)
%+ Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO)
%A Dal Lago, Ugo
%A Rioli, Alessandro
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 6th Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Mehdi Dastani
%Y Marjan Sirjani
%I Springer
%3 Fundamentals of Software Engineering
%V LNCS-9392
%P 54-68
%8 2015-04-22
%D 2015
%R 10.1007/978-3-319-24644-4_4
%Z Computer Science [cs]/Logic in Computer Science [cs.LO]Conference papers
%X 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.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01231800/document
%2 https://inria.hal.science/hal-01231800/file/main.pdf
%L hal-01231800
%U https://inria.hal.science/hal-01231800
%~ INRIA
%~ INRIA-SOPHIA
%~ INRIASO
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-LNCS-9392
%~ IFIP-FSEN
%~ UNIV-COTEDAZUR