The code includes:
- a cut-free sequent calculus (SeqCalc.agda)
- a focused subsystem of sequent calculus derivations (Focusing.agda)
- proof of Maehara-style interpolation: the interpolation procedure (Interpolation.agda), the variable condition (VarCondition.agda), the proof that interpolation is right inverse to cut (CutInterpolation.agda)
The main file containing the whole development is Main.agda.
The formalization uses Agda 2.6.2.