{"ID":2893036,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2507.13792","arxiv_id":"2507.13792","title":"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.","short_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,...","url_abs":"https://arxiv.org/abs/2507.13792","url_pdf":"https://arxiv.org/pdf/2507.13792v4","authors":"[\"Riccardo Bianchini\",\"Francesco Dagnino\",\"Paola Giannini\",\"Elena Zucca\"]","published":"2025-07-18T10:06:08Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}