Author name cluster

Daniel Hirschkoff

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.

4 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

I&C Journal 2016 Journal Article

Name-passing calculi: From fusions to preorders and types

Daniel Hirschkoff
Jean-Marie Madiot
Davide Sangiorgi

The fusion calculi are a simplification of the pi-calculus in which input and output are symmetric and restriction is the only binder. We highlight a major difference between these calculi and the pi-calculus from the point of view of types, proving some impossibility results for subtyping in fusion calculi. We propose a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. We examine the consequences of the modification on behavioural equivalence (e. g. , context-free characterisations of barbed congruence) and expressiveness (e. g. , full abstraction of the embedding of the asynchronous pi-calculus).

Details DOI

TCS Journal 2005 Journal Article

On the representation of McCarthy's amb in the π -calculus

Arnaud Carayol
Daniel Hirschkoff
Davide Sangiorgi

We study the encoding of λ [ ], the call-by-name λ -calculus enriched with McCarthy's amb operator, into the π -calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ -calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about λ [ ] that are similar to those for the encoding of pure λ -calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π -calculus, which sheds some light on the relationship between fairness and bisimilarity.

Details DOI