A note on coinduction and weak bisimilarity for while programs

Rutten, Jan

An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics O for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model D. Next O = D is proved by coinduction.

Additional Metadata
ACM	PROGRAMMING LANGUAGES (acm D.3), COMPUTATION BY ABSTRACT DEVICES (acm F.1), LOGICS AND MEANINGS OF PROGRAMS (acm F.3)
MSC	Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Semantics (msc 68Q55)
THEME	Software (theme 1)
Publisher	CWI
Series	Software Engineering [SEN]
Organisation	Computer Security
Citation APA Style AAA Style APA Style Cell Style Chicago Style Harvard Style IEEE Style MLA Style Nature Style Vancouver Style American-Institute-of-Physics Style Council-of-Science-Editors Style BibTex Format Endnote Format RIS Format CSL Format DOIs only Format	Rutten, J. (1998). A note on coinduction and weak bisimilarity for while programs. Software Engineering [SEN]. CWI.

Free Full Text ( Final Version , 398kb )

A note on coinduction and weak bisimilarity for while programs

Publication

Publication

Address

CWI researchers

Questions or comments?

A note on coinduction and weak bisimilarity for while programs

Publication

Publication

Workflow

Workflow

Add Content