SOS for Higher Order Processes

d Abstract) MohammadReza Mousavi1 , Murdoch J. Gabbay2 , and Michel A. Reniers1 1 Department of Computer Science, 2 Department of Computer Science, Eindhoven University of Technology, King’s College London, Eindhoven, The Netherlands London, UK Abstract. We lay the foundations for a Structural Operational Semantics (SOS) framework for higher order processes. Then, we propose a number of 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 the promoted tyft/tyxt format. Furthermore, we propose and prove a congruence format for a notion of higher order bisimilarity arising naturally from our SOS framework. To illustrate our formats, we apply them to Thomsen’s Calculus of Higher Order Communicating Systems (CHOCS). Key words: Formal Semantics, Structural Operational Semantics, Bisimulation, C...

• Type: Conference
• Year: 2005
• Where: CONCUR
• Authors: Mohammad Reza Mousavi, Murdoch Gabbay, Michel A. Reniers
• Keywords: Computer Science, CONCUR 2005, Structural Operational Semantics, Tyft/tyxt Format