There are a number of restrictions on the specification of operational semantics of process calculi that guarantee that the resulting bisimulation relation is a congruence. These restrictions are known variously as de Simone format, GSOS, tyft/tyxt, etc. To date, all this work has been carried our for systems described via first-order terms and first-order logic inference rules.
While a number of higher-order process calculi and calculi for mobility of names and links have been studied, no general syntactic restrictions are know for such calculi that parallel the results for first-order systems. This stage will attempt to develop such restrictions. The use of higher-order meta-logic and higher-order abstract syntax is hoped to provide a strong basis for this work.
It will be possible to continue this work as a PhD student.
R. de Simone. Higher-level synchronising devices in meije--SCCS. Theoretical Computer Science, 37:245--267, 1985.
J. F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, vol 100, pp. 202-260 (1992).
Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation Can't be Traced. Journal of the ACM, 42(1), January 1995, pp. 232-268. [pdf].
Douglas J. Howe. Proving Congruence of Bisimulation in Functional Programming Languages. Information and Computation 124(2), pp. 103--112 (1996).
Karen L. Bernstein. A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages. In the Proceedings of LICS '98, edited by John Mitchell, pp. 153-163. [ps].
D. Miller and C. Palamidessi. Foundational Aspects of Syntax. ACM Computing Surveys 31(3es):11, 1999. (DVI, PostScript, PDF)
Dale Miller and Alwen Tiu. A Proof Theory for Generic Judgments. Submitted to a special issue of the ACM Transactions on Computational Logic, edited by Phokion Kolaitis. [pdf].