Skip to Main content Skip to Navigation

Behavioral Equivalences for Higher-Order Languages with Probabilities

Valeria Vignudelli 1, 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 : Higher-order languages, whose paradigmatic example is the λ-calculus, are languages with powerful operators that are capable of manipulating and exchanging programs themselves. This thesis studies behavioral equivalences for programs with higher-order and probabilistic features. Behavioral equivalence is formalized as a contextual, or testing, equivalence, and two main lines of research are pursued in the thesis. The first part of the thesis focuses on contextual equivalence as a way of investigating the expressiveness of different languages. The discriminating powers offered by higher- order concurrent languages (Higher-Order π-calculi) are compared with those offered by higher-order sequential languages (à la λ-calculus) and by first-order concurrent languages (à la CCS). The comparison is carried out by examining the contextual equivalences induced by the languages on two classes of first-order processes, namely nondeterministic and probabilistic processes. As a result, the spectrum of the discriminating powers of several varieties of higher-order and first-order languages is obtained, both in a nondeterministic and in a probabilistic setting. The second part of the thesis is devoted to proof techniques for contextual equivalence in probabilistic λ-calculi. Bisimulation-based proof techniques are studied, with particular focus on deriving bisimulations that are fully abstract for contextual equivalence (i.e., coincide with it). As a first result, full abstraction of applicative bisimilarity and similarity are proved for a call-by-value probabilistic λ-calculus with a parallel disjunction operator. Applicative bisimulations are however known not to scale to richer languages. Hence, more robust notions of bisimulations for probabilistic calculi are considered, in the form of environmental bisimulations. Environmental bisimulations are defined for pure call- by-name and call-by-value probabilistic λ-calculi, and for a (call-by-value) probabilistic λ-calculus extended with references (i.e., a store). In each case, full abstraction results are derived.
Complete list of metadata

Cited literature [122 references]  Display  Hide  Download
Contributor : Vignudelli Valeria <>
Submitted on : Wednesday, November 22, 2017 - 12:13:38 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM


Files produced by the author(s)


  • HAL Id : tel-01644462, version 1



Valeria Vignudelli. Behavioral Equivalences for Higher-Order Languages with Probabilities. Logic in Computer Science [cs.LO]. University of Bologna, 2017. English. ⟨tel-01644462⟩



Record views


Files downloads