  Comparison of concurrent programming languages and correctness of program
transformations in concurrency are the focus of this research. As criterion we
use contextual semantics adapted to concurrency, where may -- as well as should
-- convergence are observed. We investigate the relation between the
synchronous pi-calculus and a core language of Concurrent Haskell (CH). The
contextual semantics is on the one hand forgiving with respect to the details
of the operational semantics, and on the other hand implies strong requirements
for the interplay between the processes after translation. Our result is that
CH embraces the synchronous pi-calculus. Our main task is to find and prove
correctness of encodings of pi-calculus channels by CH's concurrency
primitives, which are MVars. They behave like (blocking) 1-place buffers
modelling the shared-memory. The first developed translation uses an extra
private MVar for every communication.We also automatically generate and check
potentially correct translations that reuse the MVars where one MVar contains
the message and two additional MVars for synchronization are used to model the
synchronized communication of a single channel in the pi-calculus.Our automated
experimental results lead to the conjecture that one additional MVar is
insufficient.
