Applicative Bisimulation and Quantum λ-Calculi - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Applicative Bisimulation and Quantum λ-Calculi

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (469.97 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01231800 , version 1 (20-11-2015)

Licence

Paternité

Identifiants

Citer

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⟩
128 Consultations
136 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More