Head linear reduction

Head linear reduction is a reduction strategy for the \lambda-calculus. It arises from the following semantic approaches to higher-order computation:

game semantics
geometry of interaction
(possibly?) recursion schemes

It is the reduction strategy implemented by the Krivine abstract machine.

References

A "tutorial" introdution to head linear reduction and its relationship to the Krivine machine is given in

Danos, Vincent, and Laurent Regnier. 2004. ‘Head Linear Reduction’. pdf

@unpublished{danos_2004,
	title = {Head {Linear} {Reduction}},
	url = {http://people.cs.uchicago.edu/~brady/CSPP50102/notes/pam.pdf},
	author = {Danos, Vincent and Regnier, Laurent},
	year = {2004}
}