Using a Generalisation Critic to find Bisimulations for Coinductive Proofs - Dennis, Louise Abigail; Bundy, Alan; Green, Ian (Springer, 1999)
Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes.