  In this short paper, we consider a form of higher-order rewriting with a
call-by-value evaluation strategy so as to model call-by-value programs. We
briefly present a cost-size semantics to call-by-value rewriting: a class of
algebraic interpretations that map terms to tuples that bound both the
reductions' cost and the size of normal forms.

Logic in Computer Science