Don't exhaust, don't waste
This work addresses resource management in programming languages, offering a formal guarantee against resource misuse, but it is incremental as it builds on existing lambda calculus frameworks.
The authors extended a lambda calculus with a resource-aware type system that tracks resource usage, ensuring well-typed programs have computations where no resource is exhausted or wasted, achieved through a parametric grade algebra and big-step semantics.
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.