Small bisimulations for reasoning about higher-order imperative programs

12 years 1 months ago
Small bisimulations for reasoning about higher-order imperative programs
We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higherorder values, are storable. Our notion of bisimulation leads to smaller and more tractable relations than does the method of Sumii and Pierce [31]. In particular, our method allows one to write down a bisimulation relation directly in cases where [31] requires an inductive specification, and where the principle of local invariants [22] is inapplicable. Our method can also express examples with higher-order functions, in contrast with the most widely known previous methods [4, 22, 32] which are limited in their ability to deal with such examples. The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence. Categories and Subject Descriptors F.3.2 [Logic and Meanings of Programs]: Semantics of Programming Languages...
Vasileios Koutavas, Mitchell Wand
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Vasileios Koutavas, Mitchell Wand
Comments (0)