2020/07/20 by François Bry, Bry, François
Computer Science · #Computation and Language (cs.CL) #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2007.09909
openalex publication_date 2020/07/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle, which has been originally specified for the equality predicate only, to other predicates. This generalization makes the coinduction proof principle more intuitive and stresses its closeness with structural induction. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.