We propose an abstract framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results about congruence of bisimilarity and soundness of bisimulation up to context, in three variants of the π-calculus.
Wed 16 Jan
|13:45 - 14:07|
Tom HirschowitzUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 ChambéryLink to publication DOI File Attached
|14:07 - 14:29|
Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Lorenzo GheriMiddlesex University London, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH ZurichLink to publication DOI File Attached
|14:29 - 14:51|
Paul-André MelliesCNRS and University Paris DiderotLink to publication DOI File Attached