The Lazy Lambda Calculus in a Concurrency Scenario (Extended Abstract)

) Davide Sangiorgi LFCS - Department of Computer Science Edinburgh University Edinburgh - EH9 3JZ - UK Abstract The use of lambda calculus in richer settings, possibly involving parallelism, is examined in terms of its effect on the equivalence between lambda terms. We concentrate here on Abramsky's lazy lambda calculus and we follow two directions. First, the lambda calculus is studied within a process calculus by examining the equivalence $ induced by Milner's encoding into the -calculus. We give exact operational and denotational characterizations for $. Secondly, we examine Abramsky's applicative bisimulation when the lambda calculus is augmented with (well-formed) operators, i.e. symbols equipped with reduction rules describing their behaviour. Then, maximal discrimination is obtained when all operators are considered; we show that this discrimination coincides with the one given by $ and that the adoption of certain non-deterministic operators is sufficient and necessary...