Article contents
A focused linear logical framework and its application to metatheory of object logics
Published online by Cambridge University Press: 15 November 2021
Abstract
Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 31 , Special Issue 3: Logical and Semantic Frameworks with Applications , March 2021 , pp. 312 - 340
- Copyright
- © The Author(s), 2021. Published by Cambridge University Press
References
- 3
- Cited by