Call-by-value Solvability

Abstract

The notion of solvability in the call-by-value λ -calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical β -reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment system, assigning types of a given shape to all and only the call-by-value solvable terms.