Verified memoization and dynamic programming

DOI10.1007/978-3-319-94821-8_34MaRDI QIDQ1791205zbMATH OpenOpenAlexFDO

Authors Simon Wimmer, Shuwei Hu, Tobias Nipkow

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_34

Mathematics Subject Classification ID

Dynamic programming (90C39) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Recursion Schemes for Dynamic Programming
• Efficient memo-table management strategies
• Imperative Functional Programming with Isabelle/HOL
• Refinement to Imperative/HOL
• The Isabelle collections framework

Cited in

(7)

• Efficient memo-table management strategies
• Automated verification of the parallel Bellman-Ford algorithm
• A bounds inference method for vector-based memoization
• Effect polymorphism in higher-order logic (proof pearl)
• Recursion Schemes for Dynamic Programming
• Partial memoization for obtaining linear time behavior of a 2DPDA
• Contract-based resource verification for higher-order functions with memoization

Describes a project that uses

Uses Software

• Memoization
• VerifyThis
• Isabelle/HOL
• Coq

This page was built for publication: Verified memoization and dynamic programming

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