Productivity Verification for Functional Programs by Reduction to Termination Verification

Productivity Verification for Functional Programs by Reduction to Termination Verification

Explore a novel method for verifying productivity in functional programs generating co-inductive data structures. Learn how this approach transforms co-inductive data structures into functions, reducing the productivity verification problem to a termination problem for call-by-name higher-order functional programs. Discover the formalization and correctness proof of this transformation, as well as its implementation in an automated productivity checker. Gain insights into co-inductive types, automated program verification, and higher-order functional programs through this 23-minute video presentation from the PEPM 2024 conference.