A Contextual Formalization of Structural Coinduction

Learn about structural coinduction as a dual technique to structural induction for understanding corecursive programs through this 25-minute conference presentation from ICFP 2025. Explore how structural coinduction can be used to reason about programs based solely on the logical structure of their context, with the speakers demonstrating informal proof techniques that mirror the style of inductive proofs while ensuring complete case coverage and correct use of coinductive hypotheses. Discover the formalization of this intuitive concept through a syntactic theory for deriving program equalities, which is grounded in the computational behavior of abstract machines and proven sound with respect to observational equivalence. Gain insights into this advanced topic in functional programming and formal methods as presented by researchers from the University of Massachusetts at Lowell and University of Oregon at the ACM SIGPLAN-sponsored International Conference on Functional Programming.