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+ , meta logic for the linear logical framework LLF [CP96] 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.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Andrew McCreight, Carsten Schürmann
• Keywords: ENTCS 2008, Linear Logical Framework, Logic, Logical Framework