@inproceedings{f8294f8a56094f3aa1c5a9cb64580a68,
title = "Bisimulations for probabilistic linear lambda calculi",
abstract = "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.",
keywords = "Bisimulation, Contextual equivalence, Full abstraction, Probabilistic lambda calculi",
author = "Yuxin Deng and Yuan Feng",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017 ; Conference date: 13-09-2017 Through 15-09-2017",
year = "2017",
month = jul,
day = "2",
doi = "10.1109/TASE.2017.8285625",
language = "英语",
series = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1--8",
booktitle = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
address = "美国",
}