Bisimulations for probabilistic linear lambda calculi

Deng, Y; Feng, Y

Bisimulations for probabilistic linear lambda calculi

Deng, Y Feng, Y

Permalink

Publication Type:: Conference Proceeding
Citation:: Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, 2018, 2018-January pp. 1 - 8
Issue Date:: 2018-02-07

Closed Access

	Filename	Description	Size
	08285625.pdf	Published version	383.09 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

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.date.issued	2018-02-07	en_US
dc.identifier.citation	Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, 2018, 2018-January pp. 1 - 8	en_US
dc.identifier.isbn	9781538619247	en_US
dc.identifier.uri	http://hdl.handle.net/10453/127374
dc.description.abstract	© 2017 IEEE. We investigate a notion of probabilistic program equivalence under linear contexts. We show that both a statebased and a distribution-based bisimilarity are sound coinductive proof techniques for reasoning about higher-order probabilistic programs, but only the distribution-based one is complete for linear contextual equivalence. The completeness proof is novel and directly constructs linear contexts from transitions, rather than the traditional approach of characterizing bisimilarities as testing equivalences.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation.ispartof	Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017	en_US
dc.relation.isbasedon	10.1109/TASE.2017.8285625	en_US
dc.title	Bisimulations for probabilistic linear lambda calculi	en_US
dc.type	Conference Proceeding
utslib.citation.volume	2018-January	en_US
utslib.for	0803 Computer Software	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	closed_access
pubs.publication-status	Published	en_US
pubs.volume	2018-January	en_US

Abstract:

© 2017 IEEE. We investigate a notion of probabilistic program equivalence under linear contexts. We show that both a statebased and a distribution-based bisimilarity are sound coinductive proof techniques for reasoning about higher-order probabilistic programs, but only the distribution-based one is complete for linear contextual equivalence. The completeness proof is novel and directly constructs linear contexts from transitions, rather than the traditional approach of characterizing bisimilarities as testing equivalences.

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

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