We introduce a new proof technique for showing the correctness of 0CFA-like analyses with respect to small-step semantics.
We illustrate the technique by proving the correctness of 0CFA for the pure λ-calculus under arbitrary β-reduction. This result
was claimed by Palsberg in 1995; unfortunately, his proof was flawed. We provide a correct proof of this result, using a simpler
and more general proof method. We illustrate the extensibility of the new method by showing the correctness of an analysis
for the Abadi-Cardelli object calculus under small-step semantics.