Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

We study an extension of Plotkin's call-by-value lambda-calculus via twocommutation rules (sigma-reductions). These commutation rules are sufficient toremove harmful call-by-value normal forms from the calculus, so that it enjoyselegant characterizations of many semantic properties. We prove that thisextended calculus is a conservative refinement of Plotkin's one. In particular,the notions of solvability and potential valuability for this calculus coincidewith those for Plotkin's call-by-value lambda-calculus. The proof rests on astandardization theorem proved by generalizing Takahashi's approach of parallelreductions to our set of reduction rules. The standardization is weak (i.e.redexes are not fully sequentialized) because of overlapping interferencesbetween reductions.Comment: 27 page