Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus. Surprisingly, the obtained relation coincides with context equivalence, contrary to what happens when call-by-name evaluation is considered. Even more surprisingly, full-abstraction only holds in a symmetric setting. © 2014 Springer-Verlag.
CITATION STYLE
Crubillé, R., & Dal Lago, U. (2014). On probabilistic applicative bisimulation and call-by-value λ-calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 209–228). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_12
Mendeley helps you to discover research relevant for your work.