The Symbolic Applied Pi-calculus

The pi-calculus is a "pure" process algebra in that the only
messages are atomic names. While this is very convenient from
a foundational viewpoint, it also makes it very difficult to
do anything practical with it. Even models of simple protocols
tend to get either overly simplistic or very large and hard to
understand.

The applied pi-calculus can be seen as an extension of the
pi-calculus where value-passing, primitive functions, and
equations among terms has been added. This makes it much easier
to model real-world problems, but at the same time it makes
the theory more difficult. In this talk we present
the applied pi-calculus and a notion of equivalence between
processes and show how we deal with it symbolically.