Parametric parameter passing lambda-calculus

A lambda-calculus is defined, which is parametric with respect to a set V of input values and subsumes all the different lambda-calculi given in the literature, in particular the classical one and the call-by-value lambda-calculus of Plotkin. It is proved that it enjoy the confluence property, and a necessary and sufficient condition is given, under which it enjoys the standardization property. Its operational semantics is given through a reduction machine, parametric with respect to both V and a set Vo of output values.