A cost-aware logical framework
Yue Niu (1), Jonathan Sterling (1), Harrison Grodin (1), Robert Harper, (1) ((1) Carnegie Mellon University)

TL;DR
This paper introduces calf, a cost-aware logical framework that models cost as a computational effect, enabling formal analysis of algorithm complexity within a dependent type theory, and demonstrates its effectiveness through case studies in Agda.
Contribution
It presents calf, a novel dependent type theory framework that integrates cost analysis with program behavior, allowing formal verification of algorithmic complexity.
Findings
Proved tight bounds for Euclid's algorithm
Verified amortized complexity of batched queues
Derived bounds for merge sort's complexity
Abstract
We present , a ost-ware ogical ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of \emph{phase distinctions}, we argue that the cost structure of programs motivates a phase distinction between and . Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques
