On coinduction and quantum lambda calculi

Deng, Y; Feng, Y; Dal Lago, U

On coinduction and quantum lambda calculi

Deng, Y Feng, Y

Dal Lago, U

Permalink

Publication Type:: Conference Proceeding
Citation:: Leibniz International Proceedings in Informatics, LIPIcs, 2015, 42 pp. 427 - 440
Issue Date:: 2015-08-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted Manuscript versionAdobe PDF (579.15 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Deng, Y	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Dal Lago, U	en_US
dc.date.issued	2015-08-01	en_US
dc.identifier.citation	Leibniz International Proceedings in Informatics, LIPIcs, 2015, 42 pp. 427 - 440	en_US
dc.identifier.isbn	9783939897910	en_US
dc.identifier.issn	1868-8969	en_US
dc.identifier.uri	http://hdl.handle.net/10453/47654
dc.description.abstract	© Yuxin Deng, Yuan Feng, and Ugo Dal Lago; licensed under Creative Commons License CC-BY. 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.	en_US
dc.relation.ispartof	Leibniz International Proceedings in Informatics, LIPIcs	en_US
dc.relation.isbasedon	10.4230/LIPIcs.CONCUR.2015.427	en_US
dc.title	On coinduction and quantum lambda calculi	en_US
dc.type	Conference Proceeding
utslib.citation.volume	42	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	42	en_US

Abstract:

© Yuxin Deng, Yuan Feng, and Ugo Dal Lago; licensed under Creative Commons License CC-BY. 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.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/47654