Bisimulations for probabilistic linear lambda calculi

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
Metrics:
Full metadata record
Files in This Item:
Filename Description Size
08285625.pdfPublished version383.09 kB
Adobe PDF
© 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: