This project implements a formalization of linear logic in Lean 4, including:
- Core syntax for linear logic formulas
- Sequent calculus rules for inference
- Examples of theorems and proofs
Linear logic, introduced by Jean-Yves Girard, is a resource-sensitive logic where assumptions must be used exactly once, unlike classical logic. This makes it well-suited for reasoning about computational resources, concurrency, and state.
Key features of linear logic formalized in this project:
- Multiplicative connectives: ⊗ (tensor), ⊸ (linear implication)
- Additive connectives: & (with), ⊕ (plus)
- Exponential modalities: ! (of course), ? (why not)
- Resource management rules based on consumption semantics
LinearLogic/Basic.lean: Core definitions and utilitiesLinearLogic/Sequent.lean: Sequent calculus implementationLinearLogic/Examples.lean: Example theorems and proofsLinearLogic/Test.lean: Test cases for the implementationMain.lean: Entry point for running the project
The project uses Lake, Lean 4's build system:
# Build the project
lake build
# Run the main executable
lake exe linear_logicThis project is available under the MIT License.