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:
© 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: