Liquid Resource Types
summary
Liquid Resource Types claims an automated refinement-type system that proves precise, value-dependent resource bounds (polynomial, exponential and fine-grained expressions) by adding inductive potentials and abstract potentials to liquid types. A prototype type checker reduces typing to solving Second-Order Conditional Linear Arithmetic constraints and verifies bounds for 12 benchmark programs including quadratic and insertion‑sort costs. The paper proves soundness against a cost-aware semantics. Current limits: only inductive potentials, no multi-variant n×m bounds and no type inference.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:55RESOURCE ANALYSIS
- 1:19EXAMPLE: INSERTION SORT
- 2:29LIQUID TYPES AND RESOURCES
- 3:25CONTRIBUTIONS
- 4:40THE POTENTIAL METHOD
- 5:19RESYN: LIQUID TYPES + LINEAR POTENTIALS
- 6:42OUTLINE
- 6:56INDUCTIVE POTENTIALS
- 8:37ABSTRACT POTENTIALS
- 9:42CONSTRAINT-BASED TYPE CHECKING
- 12:23TYPE SOUNDNESS
- 12:59REUSABLE DATATYPES
- 14:21LIQUID RESOURCE TYPES
related talks
33mResource polymorphism: proposal for integrating first-class resources into ML
18mInference of Resource Management Specifications
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
14mQuantified Underapproximation via Labeled Bunches
52mThink Abstractly, Work Concretely
22mExecution Time Program Verification With Tight Bounds
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
23mSpecifying and Verifying Future Conditions