Parametric parameter passing λ-calculus

A λ-calculus is defined, which is parametric with respect to a set V of input values and subsumes all the different λ-calculi given in the literature, in particular the classical one and the call-by-value λ-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 V o of output values.

Authors

• Luca Paolini
• Simona Ronchi Della Rocca

Keywords

• λ-Calculus
• Confluence
• Standardization