Head linear reduction is a reduction strategy for the -calculus. It arises from the following semantic approaches to higher-order computation:
It is the reduction strategy implemented by the Krivine abstract machine.
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}
}