How to make destructive updates less destructive

Abstract

We present a safe embedding of mutable data structures in functional languages. With safety we mean that confluence and (in some sense) referential transparency are maintained. We develop a static criterion based on abstract interpretation which checks that any side-effect which a function may exert via a destructive update remains invisible. The technique opens up the possibility of designing safe and efficient wide-spectrum languages which combine functional and imperative language constructs.