Abstract Structural induction is pervasively used by functional programmers and researchers for both informal reasoning as well as formal methods for program verification and semantics. In this paper, we promote its dual—structural coinduction—as a technique for understanding corecursive programs only in terms of the logical structure of their context. We illustrate this technique as an informal method of proofs which closely match the style of informal inductive proofs, where it is straightforward to check that all cases are covered and the coinductive hypotheses are used correctly. This intuitive idea is then formalized through a syntactic theory for deriving program equalities, which is justified purely in terms of the computational behavior of abstract machines and proved sound with respect to observational equivalence.

@article{paperbot3331,
  title = {A contextual formalization of structural coinduction},
  author = {PAUL DOWNEN and ZENA M. ARIOLA},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s0956796825100026}
}