Two decades of automatic amortized resource analysis

DOI10.1017/S0960129521000487OpenAlexW4220906786MaRDI QIDQ5875892

Steffen Jost, Jan Hoffmann

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

zbMATH Keywords

surveycomplexitytype systemsresource bound analysis

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• NESL

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