Environmental bisimulations for probabilistic higher-order languages are studied. In contrastwith applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe's in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as "up-to techniques," are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in nonprobabilistic languages. Some of thesemodifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.

Sangiorgi D., Vignudelli V. (2019). Environmental bisimulations for probabilistic higher-order languages. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 41(4), 1-64 [10.1145/3350618].

Environmental bisimulations for probabilistic higher-order languages

Sangiorgi D.;
2019

Abstract

Environmental bisimulations for probabilistic higher-order languages are studied. In contrastwith applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe's in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as "up-to techniques," are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in nonprobabilistic languages. Some of thesemodifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.
2019
Sangiorgi D., Vignudelli V. (2019). Environmental bisimulations for probabilistic higher-order languages. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 41(4), 1-64 [10.1145/3350618].
Sangiorgi D.; Vignudelli V.
File in questo prodotto:
File Dimensione Formato  
toplas19_postprint.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 1.21 MB
Formato Adobe PDF
1.21 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/730806
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact