A Meta Linear Logical Framework
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"@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.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
27
References
13
Citations
NaN
KQI