A note on Coinduction and Weak Bisimilarity for While Programs
Jan J. M. M. Rutten · RAIRO - Theoretical Informatics and Applications · 1999
An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model . Next is proved by coinduction.