A Linear Logical Framework

We present the linear type theory λΠ⊸&⊤ 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.

Authors

• Iliano Cervesato
• Frank Pfenning

Keywords

No keywords are indexed for this paper.