Contract-based resource verification for higher-order functions with memoization

DOI10.1145/3009837.3009874zbMATH Open1380.68099OpenAlexW2565399133MaRDI QIDQ5370871FDOQ5370871

Authors: Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak 

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3009837.3009874

Recommendations

• Automatic amortised analysis of dynamic memory allocation for lazy functional programs
• Static determination of quantitative resource usage for higher-order programs
• Computer Science Logic
• Verified memoization and dynamic programming
• Towards automatic resource bound analysis for OCaml

zbMATH Keywords

dynamic programmingcomplexitylazy evaluation

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Cited In (7)

• Title not available (Why is that?)
• Exponential automatic amortized resource analysis
• Runtime verification of contracts with Themulus
• Title not available (Why is that?)
• Formula normalizations in verification
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

This page was built for publication: Contract-based resource verification for higher-order functions with memoization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370871)