  The invariance thesis of Slot and van Emde Boas states that all reasonable
models of computation simulate each other with polynomially bounded overhead in
time and constant-factor overhead in space. In this paper we show that a family
of strong call-by-value strategies in the $\lambda$-calculus are reasonable for
time. The proof is based on a construction of an appropriate abstract machine,
systematically derived using Danvy et al.'s functional correspondence that
connects higher-order interpreters with abstract-machine models by a
well-established transformation technique. This is the first machine that
implements a strong CbV strategy and simulates $\beta$-reduction with the
overhead polynomial in the number of $\beta$-steps and in the size of the
initial term. We prove this property using a form of amortized cost analysis
\`a la Okasaki.
