Bisimulations for probabilistic linear lambda calculi

Publication Type:
Conference Proceeding
Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, 2018, 2018-January pp. 1 - 8
Issue Date:
Filename Description Size
08285625.pdfPublished version383.09 kB
Adobe PDF
Full metadata record
© 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: