We develop an explicit two level system that allows programmers to
reason about the behavior of effectful programs.  The first level is
an ordinary ML-style type system, which confers standard properties on
program behavior.  The second level is a conservative extension of the
first that uses a {\em logic of type refinements} to check more
precise properties of program behavior.  Our logic is a fragment of
intuitionistic linear logic, which gives programmers the ability to
reason {\em locally} about changes of program state.  We provide a
generic resource semantics for our logic as well as a sound,
decidable, syntactic refinement-checking system.  We also prove that
refinements give rise to an optimization principle for programs.
Finally, we illustrate the power of our system through a number of
examples.