Before Esaïe Bauer's defense, we organize a small and informal workshop at IRIF, on July 3rd and 4th. The talks will take place in Sophie Germain building in room 3052 while the defense will be held in Amphi Turing (same building). Note that the workshop takes place immediately after PPS 2025 days organized by Hugo Herbelin and Rémy Cerda

• 14h : Welcome
• 14h15 - 15h : Olivier Laurent (LIP, CNRS & ENS Lyon) - The (Linear) Logical Structure of Excluded Middle
  

  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.
• 15h15 - 16h : Bahareh Afshari (Gothenburg University) - Demystifying mu
• 16h15 - 16h45: Free discussions

• 9h30 - 10h15 : Sonia Marin (Birmingham University) - Intuitionistic GL à la Simpson
• 10h30 - 11h15 : Anupam Das (Birmingham University) - Systems for fixed points in LL

• 13h : Esaïer Bauer's Phd Defense (in Amphi Turing)
  

  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.