PREBET , Enguerrand

We present a fully abstract encoding of λ ref , the call-by-value λ-calculus with references, in the πcalculus. By contrast with previous full abstraction results for sequential languages in the π-calculus, the characterisation of contextual equivalence in the source language uses a labelled bisimilarity. To define the latter equivalence, we...

We present a variant of the theory of compatible functions on relations, due to Sangiorgi and Pous. We show that the up-to context proof technique for bisimulation is compatible in this setting for two subsets of the pi-calculus: the asynchronous pi-calculus and a pi-calculus with immediately available names.

We study the notion of program equivalences, i.e. proving that two programs can be used interchangeably without altering the overall observable behaviour. This definition is highly dependent on the contexts in which these programs can be used; does the context have exceptions, parallelism, etc… So proofs also need to be adapted according to the...

The π-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any...

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been...

The π-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any...

The π-calculus has been advocated as a model to interpret, and give semantics to, languages withhigher-order features. Often these languages make use of forms of references (and hence viewing astore as set of references). While translations of references in π-calculi (and CCS) have appeared,the precision of such translations has not been fully...