Useful Evaluation: Syntax and Semantics (Technical Report)

Pablo Barenbaum, Delia Kesner, Mariana Milicich

This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear,…