Abstract We investigate how various forms of bisimulation can be characterised using the technology of logical relations. The approach taken is that each form of bisimulation corresponds to an algebraic structure derived from a transition system, and the general result is that a relation R between two transition systems on state spaces S and T is a bisimulation if and only if the derived algebraic structures are in the logical relation automatically generated from R. We show that this approach works for the original Park–Milner bisimulation and that it extends to weak bisimulation, and branching and semi-branching bisimulation. The paper concludes with a discussion of probabilistic bisimulation, where the situation is slightly more complex, partly owing to the need to encompass bisimulations that are not just relations.

We introduce the notion of higher dimensional multigraph. This notion extends that of multigraph, which underlies multicategories and is essentially equivalent to the notion of context-free grammar. We develop the definition and explain how it gives a semantically coherent category theoretic approach to the notion of higher order context-free grammar. It also gives a conceptual framework in which one can study rewrites, and rewrites of rewrites, etcetera, for proofs of sequent calculus. The definition involves a subtle interaction between geometry and linearly defined syntax; we explore the latter here, outlining the geometric intuition.

Lambek used categories with indeterminates to capture explicit variables in simply typed λ-calculus. He observed that such categories with indeterminates can be described as Kleisli categories for suitable comonads. They account for ‘functional completeness’ for Cartesian (closed) categories. Here we refine this analysis, by distinguishing ‘contextual’ and ‘functional’ completeness, and extend it to polymorphic λ-calculi. Since the latter are described as certain fibrations, we are lead to consider indeterminates, not only for ordinary categories, but also for fibred categories. Following a 2-categorical generalisation of Lambek's approach, such fibrations with indeterminates are presented as 'simple slices' in suitable 2-categories of fibrations; more precisely, as Kleisli objects. It allows us to establish contextual and functional completeness results for some polymorphic calculi.