A Meta Linear Logical Framework
Andrew McCreight, Carsten Schürmann · Electronic Notes in Theoretical Computer Science · 2008
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 ω + , 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 ω + is first-order, intuitionistic, and not linear. The soundness of L ω + is shown.