一句话：在参数化 grade 代数下为带资源标注的大步语义 λ 演算建立资源感知的类型可靠性，并用余归纳技术完成证明。
论文关注如何在语言语义中显式追踪资源消耗，并让类型系统保证良类型程序存在不耗尽所需资源的计算。作者在一个带有常见构造的 λ 演算上扩展语义与类型系统：归约过程被仪器化以记录资源使用，类型系统则在标准可靠性之外额外给出资源感知的可靠性保证。该扩展以任意 grade 代数为参数，无需对底层语言做专门改动，因而具有较好的通用性。技术上，为了让资源感知性质与语言构造的求值方式自然对应，语义采用大步风格形式化；这使可靠性性质的表述与证明变得困难，作者借助近期基于余归纳（coinductive）推理的技术来克服这一困难。
We extend the semantics and type system of a lambda calculus equipped with common constructs to be 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 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.
@article{paperbot1877,
title = {Resource-Aware Soundness for Big-Step Semantics},
author = {Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622843}
}