×

Mechanizing focused linear logic in Coq. (English) Zbl 1433.68586

Alves, Sandra (ed.) et al., Selected papers of the 12th workshop on logical and semantic frameworks, with applications (LSFA 2017), Brasilia, Brazil, September 23–24, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 338, 219-236 (2018).
Summary: Linear logic has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. Linear logic’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. Cut-elimination guarantees that linear logic is consistent and has the so-called sub-formula property. Focusing is a discipline for proof search that was introduced to reduce the search space, but has proved to have more value, as it allows one to specify the shapes of proofs available. This paper formalizes first-order linear logic in Coq and mechanizes the proof of cut-elimination and the completeness of focusing. Moreover, the implemented logic is used to encode an object logic, such as in a linear logical framework, and prove adequacy.
For the entire collection see [Zbl 1403.68008].

MSC:

68V20 Formalization of mathematics in connection with theorem provers
03B35 Mechanization of proofs and logical operations
03F05 Cut-elimination and normal-form theorems
03F52 Proof-theoretic aspects of linear logic and other substructural logics
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Coq; HYBRID
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andreoli, J.-M., Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation (1992) · Zbl 0764.03020
[2] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions, (Texts in Theoretical Computer Science. Texts in Theoretical Computer Science, EATCS Series (2004)) · Zbl 1069.68095
[3] Chaudhuri, K.; Lima, L.; Reis, G., Formalized meta-theory of sequent calculi for substructural logics, Electr. Notes Theor. Comput. Sci., 332, 57-73 (2017) · Zbl 1401.03033
[4] Chlipala, A., Parametric higher-order abstract syntax for mechanized semantics, (Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP (2008)) · Zbl 1323.68184
[5] Dawson, J. E.; Goré, R., Generic Methods for Formalising Sequent Calculi Applied to Provability Logic, (Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17 (2010)) · Zbl 1307.03033
[6] Despeyroux, J.; Felty, A. P.; Hirschowitz, A., Higher-Order Abstract Syntax in Coq, (Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA (1995)) · Zbl 1063.68650
[7] Despeyroux, J.; Olarte, C.; Pimentel, E., Hybrid and Subexponential Linear Logics, Electronic Notes in Theoretical Computer Science (2017), in press · Zbl 1395.03034
[8] DeYoung, H.; Caires, L.; Pfenning, F.; Toninho, B., Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication, (Computer Science Logic, CSL’12 (2012)) · Zbl 1252.03141
[9] Felty, A. P.; Momigliano, A., Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax, Journal of Automated Reasoning (2012) · Zbl 1252.68252
[10] Felty, A. P.; Momigliano, A.; Pientka, B., The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey, Journal of Automated Reasoning (2015) · Zbl 1357.68198
[11] Gentzen, G., Investigations into Logical Deductions, (The Collected Papers of Gerhard Gentzen (1969), North-Holland), 68-131
[12] Girard, J.-Y., Linear logic, Theoretical Computer Science (1987) · Zbl 0647.03016
[13] Graham-Lengrand, S., Polarities & Focussing: a journey from Realisability to Automated Reasoning (2014), Université Paris-Sud, Habilitation thesis
[14] Kalvala, S.; Paiva, V. D., Mechanizing linear logic in Isabelle, (10th International Congress of Logic, Philosophy and Methodology of Science (1995))
[15] Miller, D.; Palamidessi, C., Foundational Aspects of Syntax, ACM Computing Surveys (1999)
[16] Miller, D.; Pimentel, E., A formal framework for specifying sequent calculus proof systems, Theoretical Computer Science (2013) · Zbl 1259.03077
[17] Nigam, V.; Miller, D., A Framework for Proof Systems, Journal of Automated Reasoning (2010) · Zbl 1242.03057
[18] Nigam, V.; Olarte, C.; Pimentel, E., A General Proof System for Modalities in Concurrent Constraint Programming, (Concurrency Theory (CONCUR) (2013)) · Zbl 1390.68485
[19] Olarte, C.; Pimentel, E.; Nigam, V., Subexponential concurrent constraint programming, Theoretical Computer Science (2015) · Zbl 1332.68027
[20] Pfenning, F., Structural Cut Elimination, Information and Computation (2000) · Zbl 1005.03049
[21] Pfenning, F.; Elliott, C., Higher-order Abstract Syntax, (ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (1988))
[22] Power, J.; Webster, C., Working with linear logic in coq, (12th International Conference on Theorem Proving in Higher Order Logics (1999)), 1-16
[23] Reed, J., A Hybrid Logical Framework (2009), Carnegie Mellon University, PhD thesis
[24] Simmons, R. J., Structural focalization (2011), CoRR · Zbl 1354.03087
[25] Troelstra, A. S.; Schwichtenberg, H., Basic Proof Theory (2000), Cambridge University Press · Zbl 0957.03053
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.