Skip to Main content Skip to Navigation
Conference papers

On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice

Ugo Dal Lago 1, 2 Francesco Gavazzo 3, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Applicative bisimiliarity is a coinductively-defined program equivalence in which programs are tested as argument-passing processes. Starting with the seminal work by Abramsky, applicative bisimiliarity has been proved to be a powerful technique for higher-order program equivalence. Recently, applicative bisimiliarity has also been generalised to lambda calculi with algebraic effects, and with discrete probabilistic choice in particular. In this paper, we show that applicative bisimiliarity behaves well in a lambda-calculus in which probabilistic choice is available in a more general form, namely through an operator for sampling of values from continuous distributions. Our main result shows that applicative bisimilarity is sound for contextual equivalence, hence providing a new reasoning principle for higher-order probabilistic languages.
Document type :
Conference papers
Complete list of metadata

Cited literature [61 references]  Display  Hide  Download
Contributor : Francesco Gavazzo <>
Submitted on : Wednesday, January 8, 2020 - 10:01:01 AM
Last modification on : Friday, July 9, 2021 - 5:18:01 PM
Long-term archiving on: : Thursday, April 9, 2020 - 12:13:13 PM


Files produced by the author(s)


  • HAL Id : hal-02386083, version 1



Ugo Dal Lago, Francesco Gavazzo. On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice. MFPS 2019 - 35th Conference on the Mathematical Foundations of Programming Semantics, Jun 2019, London, United Kingdom. ⟨hal-02386083⟩



Record views


Files downloads