A Cellular Howe Theorem

We introduce a categorical framework for operational semantics, in which we define substitution-closed bisimilarity, an abstract analogue of the open extension of Abramsky's applicative bisimilarity. We furthermore prove a congruence theorem for substitution-closed bisimilarity, following Howe's method. We finally demonstrate that the framework covers the call-by-name and call-by-value variants of λ-calculus in big-step style. As an intermediate result, we generalise the standard framework of Fiore et al. for syntax with variable binding to the skew-monoidal case.