Resource-Aware Soundness for Big-Step Semantics
summary
Extends a call-by-value language with grades that track resource use at evaluation time and a matching graded type system, proving that well-typed programs admit a run that never exhausts needed resources. Formal contributions: a big-step semantics parametric on an arbitrary grade algebra that instruments environments and result multiplicities, coinductive, generalized-inference-system machinery to model divergence and prove soundness (coinductive proof via generalized inference systems). Works for full recursion and equi-recursive types and requires no syntax changes, but guarantees only the existence of a non-stuck run under nondeterministic consumption.
AI-written summary · about