Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
418389 | Computer Languages, Systems & Structures | 2012 | 18 Pages |
We examine different approaches to reasoning about program equivalence in a higher-order language which incorporates a basic notion of state: references of unit type (names). In particular, we present three such methods stemming from logical relations, bisimulation techniques and game semantics respectively. The methods are tested against a surprisingly difficult example equivalence at second order which exploits the intricacies of the language with respect to privacy and flow of names, and the ensuing notion of local state.
► Proving program equivalences in a language with a minimal local state effect. ► Crash course on logical relations, environmental bisimulations and game semantics. ► Rectification of a proof in nominal game semantics from 2004.