Don't exhaust, don't waste

TL;DR

This paper introduces a resource-aware extension to lambda calculus semantics and type system, ensuring programs neither exhaust nor waste resources, with a parametric approach adaptable to various usage models.

Contribution

It develops a parametric resource-aware semantics and type system for lambda calculus, guaranteeing resource correctness without language modifications.

Findings

Semantics tracks resource usage and prevents exhaustion or waste.

Type system guarantees resource-safe computations for well-typed programs.

Uses coinductive reasoning to prove resource-aware soundness.

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.