*Semantics Club 29 11 2000*

# Semantics of Value- and Name-Passing Calculi

(joint work with Marcelo Fiore)### Abstract

In [TP97] a first step was made towards a mathematical
operational semantics guaranteeing that a parametric notion of
bisimulation be a congruence. For a particular choice of the
parameters, such mathematical operational semantics was shown to
be in 1-1 correspondence with GSOS, the most well-known syntactic
format used to ensure compositionality.
The promise at the time was that the use of different parameters
would lead to the discovery of new formats for process algebras,
most notably process algebras with binding operators (such as those
used in CCS with value-passing and the pi-calculus) which had proved
prohibitive to handle so far.

Using the categorical approach to abstract syntax with variable
binding introduced in [FPT99], we are now in the position to apply
[TP97] and obtain generalized GSOS formats for value-passing
and for name-passing. I will show how to obtain (for free!)
congruence/compositionality results for both *late* and
*early* bisimulation for both name- and value-passing calculi.

### References

[FPT99] M. Fiore, G. Plotkin, D. Turi:
Abstract
Syntax and Variable Binding,
LICS'99

[TP97] D. Turi, G. Plotkin:
Towards a
Mathematical Operational Semantics,
LICS'97