On Coinduction and Quantum Lambda Calculi

Yuxin Deng 1 Yuan Feng 2 Ugo Dal Lago 3, 4
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.
Type de document :
Communication dans un congrès
Proceedings of CONCUR 2015, 2015, Madrid, Spain. LIPIcs, 42, 2015, 〈10.4230/LIPIcs.CONCUR.2015.427〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01231782
Contributeur : Ugo Dal Lago <>
Soumis le : jeudi 3 décembre 2015 - 10:15:39
Dernière modification le : jeudi 11 janvier 2018 - 16:48:55
Document(s) archivé(s) le : vendredi 28 avril 2017 - 13:54:16

Fichier

28.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Collections

Citation

Yuxin Deng, Yuan Feng, Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. Proceedings of CONCUR 2015, 2015, Madrid, Spain. LIPIcs, 42, 2015, 〈10.4230/LIPIcs.CONCUR.2015.427〉. 〈hal-01231782〉

Partager

Métriques

Consultations de la notice

219

Téléchargements de fichiers

52