TY - JOUR
T1 - Behavioral and coinductive rewriting
AU - Goguen, Joseph
AU - Lin, Kai
AU - Roşu, Grigore
N1 - Funding Information:
1 The research reported in this paper has been supported in part by National Science Foundation grant CCR-9901002, and by the CafeOBJ project of the Information Promotion Agency (IPA), Japan, as part of its Advanced Software Technology Program.
PY - 2000
Y1 - 2000
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0009898172&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0009898172&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(05)80128-8
DO - 10.1016/S1571-0661(05)80128-8
M3 - Conference article
AN - SCOPUS:0009898172
SN - 1571-0661
VL - 36
SP - 2
EP - 23
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
T2 - The 3rd International Workshop on Rewriting Logic and its Applications
Y2 - 18 September 2000 through 20 September 2000
ER -