Inductive Useful Open Call-by-Value Evaluation with Quantitative Semantics

This work establishes the first inductive definition of useful open call-by-value evaluation, and proposes a quantitative semantic interpretation of this evaluation strategy using non-idempotent intersection types.