An implementation of a so called Krivine machine, a call-by-name machine for lambda calculus, extended with continuations and a control instruction. This extension enables the machine to type classical logic where it otherwise would only type intuitionistic logic.
Krivine, J. L. (2007). A call-by-name lambda-calculus machine. Higher-order and symbolic computation, 20, 199-207.