Verification of programs that destructively manipulate data

AbstractWe investigate various equivalence relations between expressions in a first-order functional programming language augmented with the ability to destructively alter the underlying data. To define the semantics we introduce the notion of a memory structure. A computation theory for lexically scoped functional language is then defined over these structures. The equivalence relations are then defined within this model theoretic framework. A distinction is made between intensional relations and extensional relations. The former class turn out to have a much more manageable theory than the latter. The principal intensional relation studied is strong isomorphism, its properties allow for elegant verification proofs in a style similar to that of purely applicative languages. In particular the relation is preserved under many standard syntactic manipulations and transformations