Don't exhaust, don't waste
Abstract
We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, and is stuck, besides in case of type errors, if either a needed resource is exhausted, or a provided resource would be wasted. In such way, the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no resource gets either exhausted or wasted. The extension is parametric on an arbitrary "grade algebra", modeling an assortment of possible usages, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.
Cite
@article{arxiv.2507.13792,
title = {Don't exhaust, don't waste},
author = {Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca},
journal= {arXiv preprint arXiv:2507.13792},
year = {2026}
}
Comments
Preprint submitted to JFP (Journal of Functional Programming)