  We study an extension of Plotkin's call-by-value lambda-calculus via two
commutation rules (sigma-reductions). These commutation rules are sufficient to
remove harmful call-by-value normal forms from the calculus, so that it enjoys
elegant characterizations of many semantic properties. We prove that this
extended calculus is a conservative refinement of Plotkin's one. In particular,
the notions of solvability and potential valuability for this calculus coincide
with those for Plotkin's call-by-value lambda-calculus. The proof rests on a
standardization theorem proved by generalizing Takahashi's approach of parallel
reductions to our set of reduction rules. The standardization is weak (i.e.
redexes are not fully sequentialized) because of overlapping interferences
between reductions.

Logic in Computer Science