In this blog post, we give an insight into the confluence of the sequent calculus, a property mainly considered since the discovery of the so-called Curry-Howard correspondence [1]. Confluence is often thought to be part of the well-understood folklore. For people already aware of the links between intuitionism and computation, it may feel natural and…
