Monadic encapsulation in ML

In a programming language with procedures and assignments, it is often impo rtant to isolate uses of state to particular program fragments. The framewo rks of type, region, and effect inference, and monadic state are technologi es that have been used to state and enforce the property that an expression has no visible side-effects. This property has been exploited to justify t he deallocation of memory regions despite the presence of dangling pointers . Starting from an idea developed in the context of monadic state in Haskell, we develop an ML-like language with full assignments and an operator that enforces the encapsulation of effects. Using this language, we formalize an d prove the folklore connection between effect masking and monadic encapsul ation. Then, by employing a novel set of reductions to deal with dangling p ointers, we establish the soundness of the type-based encapsulation with a proof based on a standard subject reduction argument.