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.

翻译：我们扩展了一个具备常见构造的Lambda演算的语义和类型系统，使其具备“资源感知”能力。即，该语义能够追踪资源的使用情况，并且在出现类型错误之外，若所需资源耗尽或提供的资源将被浪费，则计算会陷入停滞。通过这种方式，类型系统除了保证标准的可靠性外，还确保了良类型程序存在一种计算路径，其中任何资源既不会耗尽也不会浪费。该扩展以任意一种“等级代数”（grade algebra）为参数，可模拟多种可能的资源使用方式，且无需对底层语言进行特定修改。为此，语义需以大步风格的形式化表示；作为结果，表达并证明（资源感知）可靠性具有挑战性，我们通过应用基于余归纳推理的最新技术来实现这一目标。