08/07/2020

A Cellular Howe Theorem

Peio Borthelle, Tom Hirschowitz, and Ambroise Lafont

Keywords: congruence, category theory, operational semantics, bisimilarity, Howe's method

Abstract: 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.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers