On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi

Raphaëlle Crubillé 1 Ugo Dal Lago 2, 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01091564
Contributor : Ugo Dal Lago <>
Submitted on : Friday, December 5, 2014 - 4:12:38 PM
Last modification on : Saturday, January 27, 2018 - 1:31:25 AM
Long-term archiving on : Monday, March 9, 2015 - 6:04:33 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Raphaëlle Crubillé, Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi. 23rd European Symposium on Programming, Apr 2014, Grenoble, France. ⟨10.1007/978-3-642-54833-8_12⟩. ⟨hal-01091564⟩

Share

Metrics

Record views

248

Files downloads

191