We study how to extend Linear Logic with the axiom of excluded middle while preserving cut admissibility. This leads to the introduction of the 'global contraction' rule. We show how to adapt a cut-elimination proof for standard linear logic to this additional rule. The new system validates excluded middle without making the classical contraction rule admissible (which thus happens to be a strictly stronger principle).
If time permits, we will discuss the case of variants of the excluded-middle axiom together with their associated (non-standard) structural rules.

After Craig’s seminal results on interpolation theorem, a number and variety of proof-techniques have been designed to establish interpolation theorems. Among them, Maehara’s method is specific due to its applicability to a wide range of logics admitting cut-free complete proof systems.
By reconsidering Maehara’s method, I will how one can extract a “proof-relevant” interpolation theorem for first-order linear-logic stated as follows: if π is a cut-free proof of A⊢B, we can find (i) a formula C in the common vocabulary of A and B and (ii) proofs π1 of A⊢C and π2 of C⊢B such that the proof π′ of A⊢B, obtained by cutting π1 with π2 on C, normalizes to π by cut-reduction. I will carry out this study of proof-relevant interpolation in two frameworks:
First, in the traditional sequent calculus, I will show that interpolation can be organized in two phases, bottom-up and top-down, the top-down phase solving the interpolation problem, by introducing cuts to synthesize the interpolant. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction to classical and intuitionistic logics, satisfying Craig as well as Lyndon's constraints on the vocabulary of the interpolant.
Then, I will move to Curien & Herbelin's "duality of computation" framework and prove a computational version of the above result in System L. System L is in Curry-Howard correspondence with sequent proofs allowing to analyze the computational content of Maehara's interpolation can therefore be understood as the factorization of a computation into a term and an evaluation context which interact through an interface-type, the interpolant.
After discussing how the result relates to a proof-relevant refinement of Prawitz’ proof of the interpolation theorem in natural deduction discovered by Čubrić in the 90’s for the simply typed λ-calculus, I will then turn to the question on the requirement needed to carry out this proof-relevant Maehara's method. While Maehara's method relies strongly both on (i) the tree structure of sequent proofs and (ii) their wellfoundedness, I will outline how our method can be extended (i) to proof nets, that are graphs where the order of inference rules has been forgotten, expoiting their correctness criteria, as well as (ii) to circular proofs in logics with fixed-points, where proofs contain cycles and wellfounded of proof objects is relaxed. This last part of the talk is based on joint works with Guido Fiorillo and Daniel Osorio.

This thesis focuses on non-wellfounded proof theory. While these logics emerged more recently than their wellfounded counterparts, they possess a rich theory and have numer- ous applications in areas such as programming language theory and program verification. This thesis contributes to the development of tools for the syntactic study of these log- ics, with particular emphasis on cut-elimination. We provide a comprehensive study of syntactic cut-elimination for non-wellfounded proof theory in linear logic and apply it to complex logical systems.
We begin by reviewing, in a background chapter, basic notions of proof theory (both wellfounded and non-wellfounded versions). We also provide brief introductions to lin- ear logic and modal logic. Additionally, we present concepts from Gale-Stewart games and Martin’s determinacy theorem, which we adapt to Gale-Stewart games over formula occurrences in multiplicative and additive linear logic.
In the first part of this thesis, we show how to extend existing cut-elimination results to linear logic with super exponentials, a system inspired by Nigam and Miller’s subex- ponentials. We employ a simple translation into non-wellfounded linear logic, yielding a modular approach that is readily adaptable to potential future extensions of these logics. We apply this result to a linear version of the modal µ-calculus and derive a syntactic cut-elimination result for Kozen’s non-wellfounded modal µ-calculus.
In the second part, we prove a convergence property for cut-reduction sequences in the sliced system of multiplicative and additive linear logic, using a novel proof technique that combines a proof-theoretic study of formula sequences in proofs, called threads, with Martin’s determinacy theorem. This enables us to derive a simple characterization of sequences converging to cut-free valid proofs. Finally, we demonstrate how to extend these results to full linear logic and establish a new proof of strong normalization for wellfounded linear logic.