An interesting detail from the paper is why it is called "LAMBDA". That is because in the original notation what current-day programmers would call formal argument of a function were denoted by putting an upward arrow-head on top of variable/name but since that could not be type-set easily the arrow-head was moved in front of such variable which resembles the Greek letter "lambda".