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

complexitydynamic programminglazy evaluation

Mathematics Subject Classification ID

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

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

(8)

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

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)