Behavioral and Coinductive Rewriting (invited talk)
Joseph A. Goguen, Kai Lin, Grigore Roşu · Electronic Notes in Theoretical Computer Science · 2000
Behavioral rewriting differs from standard rewriting in taking account of the weaker inference rules of behavioral logic, but it shares much with standard rewriting, including notions like termination and confluence. We describe an efficient implementation of behavioral rewriting that uses standard rewriting. Circular coinductive rewriting combines behavioral rewriting with circular coinduction, giving a surprisingly powerful proof method for behavioral properties; it is implemented in the BOBJ system, which is used in our examples. These include several lazy functional stream program equivalences and a behavioral refinement.