Date Added: Jul 2010
The authors present a technique for higher-order representation of sub-structural logics such as linear or modal logic. They show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, meta-theoretic proofs about such logics can easily be developed in the Twelf proof assistant. The Logical Framework (or LF) provides a powerful and flexible framework for encoding deductive systems such as programming languages and logics. LF employs an elegant account of binding structure by identifying object-language variables with LF variables, object-language contexts with (fragments of) the LF context, and object-language binding occurrences with LF lambda abstraction.