A Reusable Machine-Calculus for Automated Resource Analyses
summary
Claims a reusable, machine-level intermediate representation that encodes evaluation contexts as data and yields automated amortized resource bounds by combining CPS/CbPV translation, linear typing, an effect-based state token for allocation/free, and first-order parameter inference. The implemented tool autobill is open source, handles ML-like and CbPV inputs, emits first-order constraints solved with a solver/optimizer pipeline, and recovers the expected linear bound for the two-list queue example. Work separates front ends from the constraint solver but notes a need for stronger solvers and region semantics.
AI-written summary · about
chapters (17)
- 0:00Welcome
- 0:25Reusable machine calculus overview
- 1:07Automated resource analysis goals
- 4:24Cost semantics and potential functions
- 9:23Lambda calculus limitations
- 11:14Abstract machine and defunctionalized CPS
- 14:28Polarized evaluation semantics
- 16:37Data structures and parameterized types
- 18:19Stack representation and contexts
- 20:08Role of polarization
- 21:34Typing judgments and constraints
- 23:20Encoding languages in machine
- 25:53Effect system for state
- 28:29Full analysis pipeline
- 31:37Advantages of the intermediate representation
- 32:59Open problems and future
- 34:02Q&A
related talks
12mImplementing Hybrid Resource Analysis in Resource Aware ML
15mA Modular Cost Analysis for Probabilistic Programs
15mRaising Expectations: Automating Expected Cost Analysis with Types
46mMechanizing Abstract Interpretation
15mDenotational Recurrence Extraction for Amortized Analysis
30mTowards a Verified Cost Model for Call-by-Push-Value
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
15mCompiling with Continuations, Correctly