% -*- Mode: LaTeX -*-

\section{Conclusions}
\label{sec:conclusion}

In this paper, we have presented a powerful type system which provides
a general mechanism to encapsulate low-level, imperative program
fragments into sound, high-level, functional abstractions without
imposing any single-threadedness constraint.  We achieved this by
adding a new construct to the kernel language called \tbx{close}, that
changes the {\em view} of a mutable data-structure from imperative to
a functional one. The type system statically verifies the soundness of
such a change and guarantees dynamic functional behavior for the
closed object.

We also briefly described how to extend the use of the \tbx{close}
construct to arrays and general multi-level data-structures.  Our
proposal for syntactically specifying imperative expressions that may
be closed using type annotations provides complete flexibility to the
user while enabling the type system to automatically verify the
soundness of this operation.

Our type system can be viewed as a safe trap-door to embedded
imperative programming within an overall functional setting. The user
is allowed full flexibility in constructing arbitrary functional
abstractions using a controlled imperative approach.  We believe that
this is the best way to obtain the potential benefits of imperative
programming in a functional language without obscuring parallelism and
expressive power of the underlying imperative kernel.

\section{Acknowledgments}
The research described in this paper was funded in part by the
Advanced Research Projects Agency of the Department of Defense under
Office of Naval Research contract N00014-89-J-1988.

The authors would like to thank Prof. Arvind, Xavier Leroy and Yuli
Zhou for their helpful comments and suggestions.
