In this work, we present the first semantic interpretation of useful call-by-value evaluation through a non-idempotent intersection type system called U. One first contribution of this paper is a characterisation of termination of useful call-by-value evaluation via U-typability. That is, a term is typable in system U if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system U provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of useful evaluation is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy. Our third contribution is a termination-equivalence result between standard call-by-value, which may perform erasing reductions, and useful call-by-value, which is non-erasing. To establish this result, we introduce a non-erasing restriction of standard call-by-value, a refinement that serves as an intermediate calculus bridging standard and useful call-by-value. We show that all three calculi have the same termination behaviour, and hence induce the same observational equivalence.

翻译：暂无翻译