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).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, ch. 3, pp. 197–292. Elsevier Science, Amsterdam (2001)
Astesiano, E., Giovini, A., Reggio, G.: Generalized bisimulation in relational specifications. In: Cori, R., Wirsing, M. (eds.) STACS 1988. LNCS, vol. 294, pp. 207–226. Springer, Heidelberg (1988)
Bernstein, K.L.: A congruence theorem for structured operational semantics of higher-order languages. In: Proc. of LICS 1998, pp. 153–164. IEEE CS, Los Alamitos (1998)
Bloom, B.: Structural operational semantics for weak bisimulations. TCS 146, 25–68 (1995)
Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. JACM 43(5), 863–914 (1996)
Boudol, G.: Towards a lambda-calculus for concurrent and communicating systems. In: Díaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 149–161. Springer, Heidelberg (1989)
Fokkink, W.J., van Glabbeek, R.J.: Ntyft/ntyxt rules reduce to ntree rules. I&C 126(1), 1–10 (1996)
Fokkink, W.J., Verhoef, C.: A conservative look at operational semantics with variable binding. I&C 146(1), 24–54 (1998)
Gabbay, M.J., Cheney, J.: A Sequent Calculus for Nominal Logic. In: Proc. of LICS 2004, pp. 139–148. IEEE CS, Los Alamitos (2004)
Galpin, V.: A format for semantic equivalence comparison. TCS 309(1-3), 65–109 (2003)
van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. JACM 43(3), 555–600 (1996)
Groote, J.F.: Transition system specifications with negative premises. TCS 118(2), 263–299 (1993)
Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. I&C 100(2), 202–260 (1992)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. I&C 124, 103–112 (1996)
Middelburg, C.A.: Variable binding operators in transition system specifications. JLAP 47(1), 15–45 (2001)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. I&C 186(2), 165–193 (2003)
Plotkin, G.D.: A structural approach to operational semantics. JLAP 60, 17–139 (2004)
Sands, D.: From SOS rules to proof principles: An operational metatheory for functional languages. In: Proc. of POPL 1997, pp. 428–441. ACM Press, New York (1997)
Sangiorgi, D.: The Lazy lambda calculus in a concurrency scenario. I&C 111(1), 120–153 (1994)
Sangiorgi, D.: Bisimulation for Higher-Order Process Calculi. I&C 131(2), 141–178 (1996)
Thomsen, B.: Plain CHOCS a second generation calculus for higher order processes. Acta Informatica 30(1), 1–59 (1993)
Thomsen, B.: A theory of higher order communicating systems. I&C 116, 38–57 (1995)
Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. Nordic Journal of Computing 2(2), 274–302 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mousavi, M., Gabbay, M.J., Reniers, M.A. (2005). SOS for Higher Order Processes. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_25
Download citation
DOI: https://doi.org/10.1007/11539452_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)