| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Applicative Bisimulation and Quantum λ-Calculi
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.
Cited literature [21 references]
https://hal.inria.fr/hal-01231800
Contributor : Ugo Dal Lago <>
Submitted on : Friday, November 20, 2015 - 4:54:43 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Friday, April 28, 2017 - 6:02:52 PM
Contributor : Ugo Dal Lago <>
Submitted on : Friday, November 20, 2015 - 4:54:43 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Friday, April 28, 2017 - 6:02:52 PM
File
main.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License