2026-10-06T10:54:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25472 2026-03-19T12:29:03Z ddc:004 open_access

Useful Call-by-Value: A Semantic Interpretation via Quantitative Types Barenbaum, Pablo Kesner, Delia Milicich, Mariana Lambda calculus Evaluation strategies Call-by-Value Useful Evaluation Intersection types Quantitative models Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pablo Barenbaum and Delia Kesner and Mariana Milicich 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.47 urn:nbn:de:0030-drops-254721 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.47 eng https://creativecommons.org/licenses/by/4.0/legalcode