Have to mention Shen, the strongly typed functional Lisp, whose type system is based on the Sequent Calculus.

https://shenlanguage.org/learn.html

A bit of an esoreric language, but fascinating nonetheless.

It's sort of the ugly duckling of intermediate languages. In his talks SPJ generally promotes join points: https://www.youtube.com/watch?v=Gml1m-3L47s&t=4388s https://youtu.be/LMTr8yw0Gk4?t=80 I still like the sequent calculus though. Sequent calculus is a bit more symmetric than join points and doesn't have the issue of writing a function two ways as a join point and non-joint point.

Great paper, thanks for sharing! The connection between programming language technology and formal logic, like here for sequent calculus, is one of the most fascinating things.

For anyone who struggles with the references to \lambda-\mu-\tilde{\mu}, the notion that a continuation takes multiple arguments and that "control effects arise naturally", it may be helpful to review the CEK machine first: https://burakemir.ch/post/cek-and-control/

Jones has said a few times that there's no demonstrable benefit to the sequent calculus over the lambda calculus. Here they conclude that the sequent calculus is better for term rewriting optimizations. Of course, term rewriting itself hasn't been shown to be very useful.

I can't comment on sequent calculus as a compiler IR, but in the context of programming language design I think there are some interesting benefits from using sequent calculus as a formal model. This paper goes into some details: https://dl.acm.org/doi/10.1145/3547637. (Most of the authors are also authors on the OP paper.)

I think that some of this work was hamstrung by constraints of fitting in which ghc as it already existed. But it’s a very interesting line of work

Then there's lisp which even the most basic Common Lisp compiler can do a micro math CAS in a single short file.