  This paper provides foundations for strong (that is, possibly under
abstraction) call-by-value evaluation for the lambda-calculus. Recently,
Accattoli et al. proposed a form of call-by-value strong evaluation for the
lambda-calculus, the external strategy, and proved it reasonable for time.
Here, we study the external strategy using a semantical tool, namely Ehrhard's
call-by-value multi types, a variant of intersection types. We show that the
external strategy terminates exactly when a term is typable with so-called
shrinking multi types, mimicking similar results for strong call-by-name.
Additionally, the external strategy is normalizing in the untyped setting, that
is, it reaches the normal form whenever it exists.
  We also consider the call-by-extended-value approach to strong evaluation
shown reasonable for time by Biernacka et al. The two approaches turn out to
not be equivalent: terms may be externally divergent but terminating for
call-by-extended-value.
