Two decades of automatic amortized resource analysis
From MaRDI portal
Publication:5875892
DOI10.1017/S0960129521000487OpenAlexW4220906786MaRDI QIDQ5875892
Publication date: 6 February 2023
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129521000487
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Linear types and non-size-increasing polynomial time computation.
- Automated resource analysis with Coq proof objects
- Exponential automatic amortized resource analysis
- Type-based cost analysis for lazy functional languages
- Automatic Static Cost Analysis for Parallel Programs
- Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
- Practical Foundations for Programming Languages
- A provable time and space efficient implementation of NESL
- Static prediction of heap space usage for first-order functional programs
- Polarized Substructural Session Types
- A lambda-calculus foundation for universal probabilistic programming
- Amortised Resource Analysis with Separation Logic
- Amortized Resource Analysis with Polynomial Potential
- Amortised Memory Analysis Using the Depth of Data Structures
- Efficient Type-Checking for Amortised Heap-Space Analysis
- Amortized Computational Complexity
- Decidable linear list constraints
- Purely Functional Data Structures
- Work Analysis with Resource-Aware Session Types
- Automatic amortised analysis of dynamic memory allocation for lazy functional programs
- BI as an assertion language for mutable data structures
- The strength of non-size increasing computation
- Decidable Inequalities over Infinite Trees
- Automatic Space Bound Analysis for Functional Programs with Garbage Collection
- Static determination of quantitative resource usage for higher-order programs
- Quantitative Reasoning for Proving Lock-Freedom
- Towards automatic resource bound analysis for OCaml
- Multivariate amortized resource analysis
- Programming Languages and Systems