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.

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