A useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations. We proceed as follows:

• We reformulate Shivers' analysis as a set of constraints; since the constraints are conditional inclusions, they can be solved using standard algorithms.
• We prove that any solution to the constraints is sound: two computations that differ only on variables marked as useless give the same answer up to useless variables, and hence the same answer when the answer is a constant.
• We observe that this notion of soundness is too weak to support the transformation of the analyzed program. We add additional closure conditions to the analysis and show that any solution to the new set of constraints justifies the transformation.