Time: Tuesday, September 17, 13.00.
Place: Room E3-209, Fredrik Bajersvej 7.
We introduce G-relative-pushouts (GRPO) which are a 2-categorical generalisation of Leifer and Milner's relative-pushouts (RPO). The 2-cells can be seen as generalised proofs of structural congruence. By keeping track of "how the squares commute" we are able to place reaction in terms and therefore derive more informative labelled transition systems (lts). Moreover, Leifer and Milner's result guaranteeing that the largest bisimulation on the lts is a congruence extends to the 2-categorical case. To illustrate the derivation process we shall consider a simple process calculus as well as some contexts-as-arrows categories considered previously in literature.