Krivine machine

A simple abstract machine that executes terms of the -calculus via call-by-name.

In the most common presentation, the state of a Krivine machine is a triple , where is a term, is an environment mapping names to closures, and is a stack of closures. Here, a closure is a pair of a term and an environment . The result of pushing onto a stack is written .

The machine executes as follows.