Author name cluster

Adrien Durier

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

TCS Journal 2022 Journal Article

Eager functions as processes

Adrien Durier
Daniel Hirschkoff
Davide Sangiorgi

We study Milner's encoding of the call-by-value λ-calculus into the π-calculus. We show that, by tuning the encoding to two subcalculi of the π-calculus (Internal π and Asynchronous Local π), the equivalence on λ-terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle η-equality. As behavioural equivalence in the π-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.

Details DOI

TCS Journal 2020 Journal Article

Towards ‘up to context’ reasoning about higher-order processes

Adrien Durier
Daniel Hirschkoff
Davide Sangiorgi

Proving behavioural equivalences in higher-order languages is a difficult task, because interactions involve complex values, namely terms of the language. In coinductive (i. e. , bisimulation-like) techniques for these languages, a useful enhancement is the ‘up-to context’ reasoning, whereby common pieces of context in related terms are factorised out and erased. In higher-order process languages, however, such techniques are rare, as their soundness is usually delicate and difficult to establish. In this paper we adapt the technique of unique solution of equations, that implicitly captures ‘up-to context’ reasoning, to the setting of the Higher-order π-calculus. Equations are written and solved with respect to normal bisimilarity, chosen both because of its efficiency — its clauses do not require universal quantifications on terms supplied by the external observer — and because of the challenges it poses on the ‘up-to context’ reasoning and that already show up when proving its congruence properties.

Details DOI