[milani]

Cool, I'll check them out. If it is "one of the more efficient and effective ways to implement a compiler", are we aware of any non-functional languages that use this style in their compilers? Asking since most compilers use LLVM and LLVM is in SSA form.

[antonvs]

The insight in the Kelsey paper I linked is that SSA and CPS are essentially equivalent. SSA is more or less CPS expressed at a kind of lower level, more like a bytecode. So one answer to the question is that all SSA compilers are already using a form of CPS.

If you wanted to use traditional CPS explicitly, you'd need a transformation step that converts the imperative source code into a more functional intermediate form so that it can be CPS'd. There might be benefits to that, since CPS can be easier to analyze than SSA. But I'm not aware of any real imperative compilers that do it.

There's been academic work on it, like: https://arxiv.org/abs/1202.3247

One of the potential benefits is covered in that paper: the ability to prove correctness of the transformations. That kind of thing is easier to do given the mathematical tractability of CPS, due to its connection to lambda calculus.