Krivine machine

A simple abstract machine that executes -calculus terms 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.

Define the action of an environment on a term by Given a closure , we may implicitly convert to the term .