We define lambda-seal, an untyped call-by-value lambda-calculus with
primitives for _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 in open,
dynamic settings where static techniques such as type abstraction and
logical relations are not applicable.
