Using a Generalisation Critic to find Bisimulations for Coinductive Proofs

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....

Full description

Bibliographic Details
Main Authors: Dennis, Louise Abigail, Bundy, Alan, Green, Ian
Other Authors: McCune, William
Format: Conference or Workshop Item
Published: Springer 1999
Online Access:https://eprints.nottingham.ac.uk/344/