2025/07/18 by Riccardo Bianchini, Francesco Dagnino, Bianchini, Riccardo +6
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.PL
paper · pdf · doi:10.48550/arxiv.2507.13792
published as Journal of Functional Programming, Volume 36 (August 4, 2026) jfp:17800 · Preprint submitted to JFP (Journal of Functional Programming)
openalex publication_date 2025/07/18 · openalex created_date 2025/10/10 · arxiv created 2026/07/01 · openalex updated_date 2026/07/28 · arxiv updated 2026/08/05
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.