  This paper explores two topics at once: the use of denotational semantics to
bound the evaluation length of functional programs, and the semantics of strong
(that is, possibly under abstractions) call-by-value evaluation.
  About the first, we analyze de Carvalho's seminal use of relational semantics
for bounding the evaluation length of lambda-terms, starting from the
presentation of the semantics as an intersection types system. We focus on the
part of his work which is usually neglected in its many recent adaptations,
despite being probably the conceptually deeper one: how to transfer the
bounding power from the type system to the relational semantics itself. We
dissect this result and re-understand it via the isolation of a simpler size
representation property.
  About the second, we use relational semantics to develop a semantical study
of strong call-by-value evaluation, which is both a delicate and neglected
topic. We give a semantic characterization of terms normalizable with respect
to strong evaluation, providing in particular the first result of adequacy with
respect to strong call-by-value. Moreover, we extract bounds about strong
evaluation from both the type systems and the relational semantics.
  Essentially, we use strong call-by-value to revisit de Carvalho's semantic
bounds, and de Carvalho's technique to provide semantical foundations for
strong call-by-value.
