A Meta Linear Logical Framework

Logical frameworks serve as meta languages to represent deductive systems, sometimes requiring special purpose meta logics to reason about the representations. In this work, we describe , a meta logic for the linear logical framework LLF [Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264–275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.] and illustrate its use via a proof of the admissibility of cut in the sequent calculus for the tensor fragment of linear logic. is first-order, intuitionistic, and not linear. The soundness of is shown.