On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice - Archive ouverte HAL Access content directly
Conference Papers Year :

On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice

(1, 2) , (3, 2)
1
2
3

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.
Fichier principal
Vignette du fichier
mainhal.pdf (671.31 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02386083 , version 1 (08-01-2020)

Identifiers

  • HAL Id : hal-02386083 , version 1

Cite

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⟩
13 View
60 Download

Share

Gmail Facebook Twitter LinkedIn More