  In this paper we propose an approach to reasoning about properties of
imperative programs. We assume in this context that the meanings of program
constructs are described using rules in the natural semantics style with the
additional observation that these rules may involve the treatment of state. Our
approach involves modeling natural semantics style rules within a logic and
then reasoning about the behavior of particular programs by reasoning about
proofs in that logic. A key aspect of our proposal is to use a fragment of
linear logic called Lolli (invented by Hodas and Miller) to model natural
semantics style descriptions. Being based on linear logic, Lolli can provide
logical expression to resources such as state. Lolli additionally possesses
proof-theoretic properties that allow it to encode natural semantics style
descriptions in such a way that proofs in Lolli mimic the structure of
derivations based on the natural semantics rules. We will discuss these
properties of Lolli and demonstrate how they can be exploited in modeling the
semantics of imperative programs and in reasoning about such models.
