Productivity Verification for Functional Programs by Reduction to Termination Ve...
summary
Method translates coinductive values into functions that take a path (integer list) and returns the element, turning productivity into reduction to termination of a call-by-name higher-order program. Implementation extends an HFL solver into mu HFL with integer lists and generates termination/nontermination HFL formulas. Benchmarks: tool proves most cases including examples previous type-based methods reject, but fails T1 and T38 and shows slow behavior on ref3, D1 and higher-order stream instances.
AI-written summary · about
chapters (8)
- 0:00Productivity verification intro
- 3:15Related work on productivity
- 5:05Reduction method overview
- 9:53Translation examples
- 15:28Soundness and completeness
- 16:11Implementation results
- 19:07Conclusion and future work
- 20:10Q&A
related talks
15mProducts of Recursive Programs for Hypersafety Verification
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
21mVerifying term graph optimizations using Isabelle/HOL
18mA Verified Compiler for a Functional Tensor Language
15mClosing Remarks
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
34mLiquid Haskell: Verification with Refinement Types
19mAutomated Verification of Fundamental Algebraic Laws