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

DOI10.1145/3009837.3009874MaRDI QIDQ5370871zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(7)

• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Exponential automatic amortized resource analysis
• Runtime verification of contracts with Themulus
• scientific article; zbMATH DE number 7204445 (Why is no real title available?)
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Formula normalizations in verification

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)