Call-by-value solvability, revisited

In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman’s call-by-value λ CBV calculus and from Accattoli and Kesner’s substitution calculus λ sub . In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.