A bisimulation for dynamic sealing

Abstract We define *seal, an untyped call-by-value *-calculus with primitives for protecting abstractdata by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reasoning about data abstraction inopen, dynamic settings where static techniques such as type abstraction and logical relations are not applicable. 1 Introduction 1.1 Dynamic sealing: Birth, death, and rebirth Sealing is a linguistic mechanism for protecting abstract data. As originally proposed by Morris [20, 21], it consists of three constructs: seal creation, sealing, and unsealing. A fresh seal is created for each module that defines abstract data. Data is sealed when it is passed out of the module, so that it cannot be inspected or modified by outsiders who do not know the seal; the data is unsealed again when it comes back into the module, so that it can be manipulated concretely. Data abstraction is preserved as long as the seal is kept local to the module. Originally, sealing was a dynamic mechanism. Morris also proposed a static variant [21], in which the creation and use of seals at module boundaries follow a restricted pattern that can be verified by the compiler, removing the need for run-time sealing and unsealing. Other researchers found that a similar effect could be obtained by enriching a static type system with mechanisms for type abstraction (see CLU [14], for example). Type abstraction became the primary method for achieving data abstraction in languages from CLU to the present day. It is also well understood via the theory of existential types [18]