A Linear Logical Framework

We present the linear type theory lambda^T&-o\Pi as the formal basis for LLF, a conservative extension of the logical framework LF. LLF combines the expressive power of dependent types with linear logic to permit the natural and concise representation of a whole new class of deductive systems, namely those dealing with state. As an example we encode a version of Mini-ML with mutable references including its type system and its operational semantics, and describe how to take practical advantage of the representation of its computations.