  We present an abstract machine that implements a full-reducing (a.k.a.
strong) call-by-value strategy for pure $\lambda$-calculus. It is derived using
Danvy et al.'s functional correspondence from Cr\'egut's KN by: (1)
deconstructing KN to a call-by-name normalization-by-evaluation function akin
to Filinski and Rohde's, (2) modifying the resulting normalizer so that it
implements the right-to-left call-by-value function application, and (3)
constructing the functionally corresponding abstract machine.
  This new machine implements a reduction strategy that subsumes the
fireball-calculus variant of call by value studied by Accattoli et al. We
describe the strong strategy of the machine in terms of a reduction semantics
and prove the correctness of the machine using a method based on Biernacka et
al.'s generalized refocusing. As a byproduct, we present an example application
of the machine to checking term convertibility by discriminating on the basis
of their partially normalized forms.
