## Authors: Adrien Durier, Daniel Hirschkoff and Davide Sangiorgi

## Paper Information

Title: | Eager Functions as Processes |

Authors: | Adrien Durier, Daniel Hirschkoff and Davide Sangiorgi |

Proceedings: | LICS PDF files |

Editors: | Anuj Dawar and Erich GrĂ¤del |

Keywords: | pi calculus, lambda calculus, full abstraction, call by value |

Abstract: | ABSTRACT. We study Milner's encoding of the call-by-value lambda-calculus in the pi-calculus. We show that, by tuning the encoding to two subcalculi of the pi-calculus (Internal pi and Asynchronous Local pi), the equivalence on lambda-terms induced by the encoding coincides with Lassen's eager normal form bisimilarity, extended to handle eta-equality. As behavioural equivalence in the pi-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. |

Pages: | 10 |

Talk: | Jul 09 14:40 (Session 49E) |

Paper: |