The Linear Logical Framework LLF

LLF is an LF-style type theory based on linear logic. Besides the dependent function types of LF, LLF makes available linear implication, additive conjunction and additive truth at the level of types, and the corresponding constructors and destructors at the level of objects.

The expressiveness deriving from linear logic turn LLF into a powerful logical framework. It is particularly adequate for representing problems characterized by a state that evolves with time and resource-based logics such as linear logic itself.

LLF has been implemented as part of the Twelf developing environment for LF specifications. The implementation can currently type-check and type-reconstruct LLF signatures, and allows using LLF as a higher-order linear logic programming language. We intend to extend Twelf's theorem prover for LF to handle linearity in the near future.

LLF was designed at Carnegie Mellon University by Iliano Cervesato and Frank Pfenning.

Papers

Example programs

Implementation

The current prototype is part of the Twelf developing environment and it is written using SML'97 (we used SML/NJ 110). If interested, please send mail to or for the sources and instructions to compile it.

Related pages

Last modified: 3 July 1998
Iliano Cervesato () and Frank Pfenning ()