Semantics Club 29 11 2000
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.
[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