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 L"@w^+, 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. L"@w^+ is first-order, intuitionistic, and not linear. The soundness of L"@w^+ is shown.