MohammadReza Mousavi, Murdoch J. Gabbay and Michel Reniers,, To appear in: Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), San Francisco, CA, USA, volume 3653 of Lecture Notes in Computer Science, pp. 308--322, Springer-Verlag, August 2005.
We lay the foundations for a Structural Operational Semantics (SOS) framework for higher order processes. Then, we propose a number of trivial and non-trivial extensions to Bernstein's promoted tyft/tyxt format which aims at proving congruence of strong bisimilarity for higher order processes. The extended format is called promoted PANTH. This format is easier to apply and strictly more expressive than promoted tyft/tyxt. Furthermore, we formulate and prove a congruence format for a notion of higher order bisimulation arising naturally from our SOS framework. To illustrate our formats, we apply them to Thomsen's Calculus of Higher Order Communicating Systems (CHOCS).
(Paper in .ps format in .pdf format) A presentation in in .pdf format
@InProceedings{MousaviCONCUR05,
author = "Mousavi, MohammadReza, Gabbay, Murdoch J. and Reniers, Michel A.",
title = "SOS for Higher Order Processes (Extended Abstract)",
booktitle = "Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05)",
series = "Lecture Notes in Computer Science",
volume = "3653",
pages = "308--322",
editor = "Abadi, Martin and Alfaro, Luca de",
address = "San Francisco, CA, USA",
publisher = "Springer-Verlag, Berlin, Germany",
year = "2005"
}