University of Limerick Institutional Repository

Proving the correctness of unfold/fold program transformations using bisimulation

DSpace/Manakin Repository

Show simple item record

dc.contributor.author Hamilton, Geoff W.
dc.contributor.author Jones, Neil D.
dc.date.accessioned 2012-07-18T13:36:15Z
dc.date.available 2012-07-18T13:36:15Z
dc.date.issued 2012
dc.identifier.uri http://hdl.handle.net/10344/2375
dc.description peer-reviewed en_US
dc.description.abstract This paper shows that a bisimulation approach can be used to prove the correctness of unfold/fold program transformation algorithms. As an illustration, we show how our approach can be use to prove the correctness of positive supercompilation (due to S rensen et al). Traditional program equivalence proofs show the original and transformed programs are contextually equivalent, i.e., have the same termination behaviour in all closed contexts. Contextual equivalence can, however, be di cult to establish directly. Gordon and Howe use an alternative approach: to represent a program's behaviour by a labelled transition system whose bisimilarity relation is a congruence that coincides with contextual equivalence. Labelled transition systems are well-suited to represent global program behaviour. On the other hand, unfold/fold program transformations use generalization and folding, and neither is easy to describe contextually, due to use of non-local information.We show that weak bisimulation on labelled transition systems gives an elegant framework to prove contextual equivalence of original and transformed programs. One reason is that folds can be seen in the context of corresponding unfolds. en_US
dc.language.iso eng en_US
dc.publisher Springer en_US
dc.relation.ispartofseries Perspectives of Systems Informatics: Lecture Notes in Computer Science;7162 pp. 153-169
dc.relation.uri http://dx.doi.org/10.1007/978-3-642-29709-0_15
dc.rights The original publication is available at www.springerlink.com en_US
dc.subject unfold/fold en_US
dc.subject bisimulation en_US
dc.subject transformation algorithms en_US
dc.title Proving the correctness of unfold/fold program transformations using bisimulation en_US
dc.type info:eu-repo/semantics/article en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor SFI en_US
dc.relation.projectid 03/CE2/I303_1 en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Related Items

Search DSpace


Advanced Search

Browse

My Account