Applicative Bisimulation and Quantum λ-Calculi

Ugo Dal Lago 1, 2 Alessandro Rioli 1, 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01231800
Contributor : Ugo Dal Lago <>
Submitted on : Friday, November 20, 2015 - 4:54:43 PM
Last modification on : Wednesday, October 10, 2018 - 10:09:25 AM
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

Identifiers

Citation

Ugo Dal Lago, Alessandro Rioli. Applicative Bisimulation and Quantum λ-Calculi. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. pp.54-68, ⟨10.1007/978-3-319-24644-4_4⟩. ⟨hal-01231800⟩

Share

Metrics

Record views

258

Files downloads

183