Decalf: A Directed, Effectful Cost-Aware Logical Framework

Explore a groundbreaking 18-minute video presentation from POPL 2024 introducing Decalf, a directed, effectful cost-aware logical framework. Delve into the innovative approach for studying quantitative aspects of functional programs with effects, building upon the CALF framework. Discover how Decalf extends cost accounting to effectful programs, including probabilistic choice and mutable state, by reformulating the notion of cost bounds as programs themselves. Learn about the intrinsic preorder equipping every type, allowing for informative cost estimates while maintaining behavioral integrity. Examine the application of Decalf to various examples, including pure and effectful sorting algorithms, probabilistic programs, and higher-order functions. Gain insights into the justification of Decalf through a model in the topos of augmented simplicial sets. Access supplementary materials, including reusable artifacts, to further explore this cutting-edge research in algorithm analysis, cost models, and mechanized proofs.

[POPL'24] Decalf: A Directed, Effectful Cost-Aware Logical Framework