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 s

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 https://dl.acm.org/doi/10.1145/3547637. (Most of the authors are also authors on the OP paper.)