A Quantitative Interpretation of Useful Call-by-Value

Pablo Barenbaum; Delia Kesner; Mariana Milicich

Home/Archive/arXiv

arXiv · 2610.40154

A Quantitative Interpretation of Useful Call-by-Value

Pablo Barenbaum·Delia Kesner·Mariana Milicich

View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Pablo Barenbaum, Delia Kesner, Mariana Milicich. 2026-10-29. A Quantitative Interpretation of Useful Call-by-Value. https://arxiv.org/abs/2610.40154

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Negative Translations for Affine and Lukasiewicz Logic

We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in \emph{affine logic} the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and {\it vice versa}. By contrast, in the setting of \emph{Łukasiewicz logic}, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Łukasiewicz logic but are all equivalent.

cs.LO↗

arXiv2026

A Complete Mental Temporal Logic for Intelligent Agents

In this paper, we present a mental temporal logic BPICTL together with a sound and complete axiomatization, which generalizes CTL by introducing mental modalities. A sound and complete inference system of BPICTL is given. We also prove the finite model property and decidability of BPICTL. Furthermore, we present a model checking algorithm for BPICTL.

cs.LO↗

arXiv2026

Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets

We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, over stable configuration structures, and an operational one, in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity (FRB) augmented with backward ready multiset equality, which is able to distinguish between autoconcurrency and autocausation. With respect to previous work, we thus shift the emphasis from uniquely identifying events, as done in other characterizations, to counting occurrences of identically labeled events associated with incoming transitions. This yields a more lightweight behavioral equivalence than HHPB: our bisimulations are still binary relations instead of ternary ones and do not need to incrementally build any labeling- and causality-preserving bijection for occurred events. We show that our characterizations are valid in the absence of non-local autoconflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures HHPB, and backward ready multiset logic, developed for our extension of FRB.

cs.LO↗