The λ-calculus is popular as an intermediate language for practical
compilers. But in the world of logic it has a lesser-known twin,
born at the same time, called the sequent calculus. Perhaps that
would make for a good intermediate language, too? To explore
this question we designed Sequent Core, a practically-oriented core
calculus based on the sequent calculus, and used it to re-implement
a substantial chunk of the Glasgow Haskell Compiler.
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/04/sequent-calculus-icfp16.pdf