Krivine Machine

The Krivine machine (or K-machine) [1] is a simple and natural implementation of the weak-head call-by-name reduction strategy for pure λ-terms. It can be described in just three or four rules with minimal machinery (an environment and a stack). It is an abstract machines for the implementation of functional languages. It has been used in many variants. The paper [2] gives an overview of the Krivine-machine variants.

[1] A call-by-name lambda-calculus machine, J.-L. Krivine.

[2] The Next 700 Krivine Machines, R. Douence, P. Fradet.