The call-by-value λ-calculus was defined by Plotkin in 1977, in order to model the call-by-value computation, but its theory of program approximation was not satisfactory. In fact the beta-v reduction rule introduced by Plotkin is too weak to express some important properties of the languages, like solvability. In order to refine the Plotin’s result, two research lines have been open, one based on enriching the language with new syntactical constructs, the other aiming at preserving the original syntax of the lambda-calculus, while associating to the original beta-v reduction rule of Plotkin new more refined rules preserving the semantics. I will present here some results in the latter direction, due to a group of researchers, behond myself: Carraro, Guerrieri, Kerinec, Manzonetto, Pagani, Paolini.  The first step has been to endow this calculus with two permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking some redexes that remain stuck during the reduction of a lambda-term in the original operational semantics. The enriched calculus, the lambda-v-sigma-calculus, enjoys the fundamental properties like confluence and standardisation, allows for an operational characterization of solvability and semantically is conservative with respect to the original Plotkin's calculus. A further step has been obtained by a semantical method. A class of relational models for lambda-v-sigma-calculus has been designed, based on non-idempotent intersection types. Every model in the class, beside satisfying the usual properties as soundness and adequacy, validates a further reduction rule which is a restriction of the beta-I-rule. Let the lambda-V-calculus be the calculus equipped with all the reduction rules described before: every model leaving in the class is a model for it, and satisfies an Approximation Theorem. The last step has been a further refinement of the notion of approximant arising in the models allowing for the definition of a notion of B ̈ohm(-like) tree, such that all λ-terms having the same Bo ̈hm tree are observationally equivalent. The result is a satisfying theory of program approximation in the call-by-value setting.