Resource-Aware Soundness for Big-Step Semantics

Explore a conference talk from OOPSLA2 2023 that delves into extending the semantics and type system of a lambda calculus to be resource-aware. Learn how the researchers instrument reduction to track resource usage and develop a type system that guarantees no needed resource gets exhausted in well-typed programs. Discover how this resource-aware extension is made parametric on an arbitrary grade algebra without requiring ad-hoc changes to the underlying language. Understand the challenges of expressing and proving resource-aware soundness in big-step semantics and how the researchers apply coinductive reasoning techniques to overcome these challenges. Gain insights into topics such as graded modal types and generalized inference systems as presented by researchers from the University of Genoa and the University of Eastern Piedmont.