Sciweavers

Share
ENTCS
2000

Behavioral and Coinductive Rewriting

8 years 10 months ago
Behavioral and Coinductive Rewriting
Behavioral rewriting di ers 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 con uence. We describe an e cient 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 re nement.
Joseph A. Goguen, Kai Lin, Grigore Rosu
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Where ENTCS
Authors Joseph A. Goguen, Kai Lin, Grigore Rosu
Comments (0)
books