% -*- Mode: LaTeX -*-

\begin{abstract} 

In this paper, we explore the design of a powerful type system that
provides a general mechanism to encapsulate low-level imperative
program fragments into type-safe functional abstractions without
imposing any single-threadedness constraint.  Although confluence is
the responsibility of the user, the type system guarantees that
data-structures exported out of the functional abstraction are fully
polymorphic and non-mutable and therefore can be safely embedded
within functional programs without disturbing their functionality.

We present the static and the dynamic semantics of our system for a
mini-language containing ML-like references. We describe the mechanism
of converting mutable types into functional types and prove its
soundness. Finally we discuss extensions to include arrays, tuples and
general multi-level data-structures in our framework.

\end{abstract}

