Formalization for Semi-Substructural Logics

This repository provides formal proofs developed in Agda for key results in the thesis "Proof Theory of Semi-substructural Logics." The formalization focuses on two sequent calculi and their focused variants:

• $\mathsf{SkMILL_s}$: A sequent calculus for symmetric left skew monoidal closed categories
• $\mathsf{SkNMILLA_s}$: A sequent calculus for distributive left skew monoidal categories with binary products and coproducts

For each system, we have developed comprehensive machine-checked proofs that verify:

1. Cut-freeness of the sequent calculus
2. Focused sequent calculus
3. Correctness of the focused calculus

The formalization uses Agda 2.6.4.1.