# A Rewriting Implementation of pi-calculus

We introduce a rewriting implementation of the reduction relation of
$\pi$-calculus and prove its correctness. The implementation is based
on terms with De Bruijn indices and an explicit substitution
operator. The resulting rewrite rules need to be applied modulo a
large and complex equational theory, and are only of theoretical
interest. Applying the coherence techniques introduced in a previous
paper, we transform this specification into an equivalent one that only
requires rewriting modulo associativity and commutativity. This latter
rewrite system can then be straightforwardly encoded in currently
available rewriting-based programming languages. Finally, we sketch a
possible application of this implementation as the basis for
adding input-output capabilities to such languages.