  Several evaluation notions for lambda calculus qualify as reasonable cost
models according to Slot and van Emde Boas' Invariance Thesis. A notable result
achieved by Accattoli and Dal Lago is that leftmost-outermost reduction is
reasonable, where the term representation uses sharing and the steps are
useful. These results, initially studied in call-by-name, have also been
extended to call-by-value. However, the existing formulations of usefulness
lack inductive structure, making it challenging in particular to define and
reason about type systems on top of the untyped syntax. Additionally, no
type-based quantitative interpretations exist for useful evaluation. In this
work, we establish the first inductive definition of useful evaluation for open
weak call-by-value. This new useful strategy connects to a previous
implementation of usefulness through a low-level abstract machine, incurring
only in linear time overhead, thus providing a reasonable cost model for open
call-by-value implementation. We also propose a semantic interpretation of
useful call-by-value using a non-idempotent intersection type system equipped
with a notion of tightness. The resulting interpretation is quantitative, i.e.
provides exact step-count information for program evaluation. This turns out to
be the first semantical interpretation in the literature for a notion of useful
evaluation.
