We extend the semantics and type system of a lambda calculus equipped with common constructs to be \emph{resource-aware}. That is, reduction is instrumented to keep track of the usage of resources, and the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no needed resource gets exhausted.
The resource-aware extension is parametric on an arbitrary \emph{grade algebra}, 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.