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.