FixpointFeline says: Coinduction is the proof principle dual to induction —
instead of constructing the
least fixpoint, we reason about the
greatest fixpoint. If you're new here, start with Sangiorgi's book,
then pick up Jacobs for the categorical machinery. The Pous–Sangiorgi survey is
your historical compass. Have fun in the GFP. 🐱
§ 01
Foundations
Cambridge University Press, 2011 · ISBN 978-1-107-00363-7
Induction is a pervasive tool in computer science and mathematics for defining objects and reasoning on them. Coinduction is the dual of induction and brings in quite different tools. Today, it is widely used in computer science, but also in other fields, including artificial intelligence, cognitive science, mathematics, modal logics, philosophy and physics. The best known instance of coinduction is bisimulation, mainly employed to define and prove equalities among potentially infinite objects: processes, streams, non-well-founded sets, etc.
This book presents bisimulation and coinduction: the fundamental concepts and techniques and the duality with induction. Each chapter contains exercises and selected solutions, enabling students to connect theory with practice. A special emphasis is placed on bisimulation as a behavioural equivalence for processes.
Theoretical Computer Science, Vol. 249, No. 1, 2000
In the semantics of programming, finite data types such as finite lists, have traditionally been modelled by initial algebras. Later final coalgebras were used in order to deal with infinite data types. Coalgebras, which are the dual of algebras, turned out to be suited, moreover, as models for certain types of automata and more generally, for (transition and dynamical) systems.
Using the notion of coalgebra homomorphism, the definition of bisimulation on coalgebras can be shown to be formally dual to that of congruence on algebras. Thus the three basic notions of universal algebra: algebra, homomorphism of algebras, and congruence, turn out to correspond to: coalgebra, homomorphism of coalgebras, and bisimulation, respectively. In this paper, the latter are taken as the basic ingredients of a theory called universal coalgebra.
Cambridge Tracts in Theoretical Computer Science, 2016 · ISBN 978-1-107-17789-5
A comprehensive textbook covering the mathematical theory of coalgebras from first principles, including functors, natural transformations, (bi)simulations, coinduction, invariants, fibrations, and modal logic for coalgebras. Suitable as a graduate text or self-study reference for those with a background in category theory.
[4]
A Tutorial on (Co)Algebras and (Co)Induction
SURVEY
CLASSIC
Bulletin of the EATCS, Vol. 62, pp. 222–259, 1997
Bart Jacobs and Jan Rutten wrote this foundational tutorial on (Co)Algebras and (Co)Induction, published in the Bulletin of the European Association for Theoretical Computer Science, vol. 62, 1997. Accessible introduction bridging algebra/induction and coalgebra/coinduction, using the language of category theory. A canonical starting point for newcomers.
CWI Monograph, 2019
This work explains how the notions of coalgebra and coinduction arise as the dual of the notions of algebra and induction. Since the theory of coalgebra is essentially categorical, the principles discussed form an integral part of the development. Features extensive worked exercises on streams, automata, and corecursive definitions.
[6]
Advanced Topics in Bisimulation and Coinduction
BOOK
Cambridge University Press, 2011 · ISBN 978-1-107-00525-9
The book is a pre-cursor companion to the introductory book on more advanced topics. Covers up-to techniques, coinduction for higher-order languages, probabilistic systems, and metric bisimulations. Chapters by multiple leading authors.
§ 02
Program Analysis
POPL 2013, Rome, Italy · pp. 457–468 · DOI 10.1145/2429069.2429124
The authors introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, they devise an optimisation of the classical algorithm by Hopcroft and Karp, comparing their approach to the recently introduced antichain algorithms.
The paper analyses and relates the two underlying coinductive proof methods, giving concrete examples where exponential improvements over antichains are achieved; experimental results show non-negligible improvements in practice.
HKC: bisimulation up-to-congruence >> Hopcroft-Karp >= antichain
POPL 2013, Rome, Italy · pp. 193–206 · DOI 10.1145/2429069.2429093
Commonly-known lattice-theoretic accounts of the principles underlying coinductive proofs are lacking in two key respects: they do not support compositional reasoning (breaking proofs into separate pieces that can be developed in isolation), and they do not support incremental reasoning (developing proofs interactively by starting from the goal and generalizing the coinduction hypothesis repeatedly as necessary).
In addition to presenting the lattice-theoretic foundations of parameterized coinduction, demonstrating its utility on representative examples, and studying its composition with "up-to" techniques, the paper also explores its mechanization in proof assistants like Coq and Isabelle. Unlike traditional approaches which employ syntactic "guardedness checking", parameterized coinduction offers a semantic account of guardedness, leading to faster and more robust proof development, as demonstrated using the Paco Coq library.
paco(F, r) = νX. F(r ∪ X) -- parameterized greatest fixpoint
[9]
Temporal Abstract Interpretation
PAPER
POPL 2000
POPL 2000, Boston, MA · pp. 12–25
Extends classical abstract interpretation to temporal properties using fixpoints over abstract domains, enabling the verification of liveness and safety properties of programs. Connects the Galois connection framework to greatest-fixpoint reasoning, providing a bridge between abstract interpretation and coinductive methods.
[10]
Coinductive Big-Step Operational Semantics
PAPER
Information and Computation, Vol. 207, No. 2, pp. 284–304, 2009
Proposes a coinductive formulation of big-step (natural) semantics that uniformly handles both terminating and diverging executions. Demonstrates the approach on a call-by-value functional language and proves equivalence with small-step semantics. Highly relevant for program analysis involving non-termination.
[11]
Interaction Trees: Representing Recursive and Impure Programs in Coq
PAPER
TOOL
POPL 2020 (PACMPL) · Vol. 4, POPL
Introduces Interaction Trees (ITrees), a coinductive data structure for representing potentially infinite, effectful computations in Coq. Uses Paco-style parameterized coinduction for reasoning. Provides a compositional framework for program equivalence via weak bisimulation.
§ 03
Type Theory
[12]
Copatterns: Programming Infinite Structures by Observations
PAPER
POPL 2013
POPL 2013, Rome, Italy · pp. 27–38
Introduces copatterns as a dual to pattern matching, enabling the definition of corecursive functions over coinductive types by specifying their observable components. Implemented in Agda. Provides a typed-theoretic foundation for productive coinductive programming.
[13]
Recursive Subtyping Revealed
PAPER
Journal of Functional Programming, Vol. 12, No. 6, pp. 511–548, 2002
A systematic study of coinductive subtyping for recursive types, providing uniform proofs of reflexivity, transitivity, and the subtyping algorithms. Coinduction is essential to handle the infinite unfoldings of recursive types; this paper demystifies the theory behind them.
[14]
Coinduction All the Way Up
PAPER
LICS 2016, New York · pp. 307–316
Develops the theory of "complete lattices" and companion-based up-to techniques, providing a clean categorical account of when bisimulation up-to techniques are sound. Shows that the companion subsumes all known sound up-to techniques.
[15]
Flexible Coinduction in Agda
PAPER
ITP 2021 · LIPIcs Vol. 193, pp. 13:1–13:19
Provides an Agda library for inference systems, supporting their recent generalization allowing flexible coinduction — interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive interpretation and the corresponding proof principles.
§ 04
Tools & Libraries
Open source Coq library · GitHub: snu-sf/paco
A Coq library for parametric coinduction. Implements the paco construction from [8], providing tactics for coinductive proofs in Coq that avoid the syntactic guardedness checker. Also supports up-to techniques via the "companion" construction.
OCaml implementation · ENS Lyon, 2013
Reference implementation of the HKC algorithm from [7]. Checks NFA language equivalence using bisimulation up-to-congruence. Includes an interactive web applet for exploring the algorithm's state space on user-provided automata.
[18]
Foundational Extensible Corecursion: A Proof Assistant Perspective
PAPER
TOOL
ICFP 2015 · pp. 192–204
Presents a foundational theory of corecursion for codatatypes in Isabelle/HOL, supporting a wide class of corecursive definitions via friends (a generalization of guardedness). Part of the BNF-based infrastructure for (co)datatypes in Isabelle.
[19]
Up-To Techniques Using Sized Types
PAPER
PACMPL, Vol. 2 (POPL 2018) · 43:1–43:28
Uses Agda's sized types to implement up-to techniques for bisimulation in a proof assistant setting, enabling modular coinductive reasoning without guardedness issues. Shows that several standard up-to techniques can be derived from a unified sized-type framework.
§ 05
Historical Perspective
Formal Aspects of Computing, 2019 · DOI 10.1007/s00165-019-00497-w
Bisimulation is an instance of coinduction. Both bisimulation and coinduction are today widely used, in many areas of Computer Science, as well as outside Computer Science. Over roughly the last 25 years, enhancements of the principles and methods related to bisimulation and coinduction — techniques to make proofs shorter and simpler — have become a research topic on its own. In the paper the origins and the developments of the topic are reviewed.
[21]
Origins of Bisimulation and Coinduction
SURVEY
CLASSIC
ACM Computing Surveys, Vol. 41, No. 2, 2009
Examines the origins of bisimulation and bisimilarity in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), and Set Theory. Essential reading for understanding the intellectual history of coinduction.
§ 06
Abstract Interpretation & Fixpoints
[22]
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs
PAPER
CLASSIC
POPL 1977 · pp. 238–252
The foundational paper for abstract interpretation. Presents the lattice-theoretic framework based on Galois connections and fixpoint approximations, providing the basis for both forward (least fixpoint) and backward (greatest fixpoint) analyses. Greatest fixpoints are coinductive in nature.
[23]
Coinduction Up-To in a Fibrational Setting
PAPER
CSL-LICS 2014 · pp. 20:1–20:9
Provides a categorical (fibrational) account of up-to techniques and coinductive proof methods, unifying them under a single abstract framework. Proves soundness results that subsume all previously known up-to techniques and enables their compositional use.
[24]
Complete Lattices and Up-To Techniques
PAPER
APLAS 2007 · LNCS Vol. 4807, pp. 351–366
Systematically studies up-to techniques for coinduction in the setting of complete lattices, establishing general soundness and completeness results. Foundational reference for understanding how bisimulation up-to-X relates to the greatest fixpoint in the standard lattice.