I am a third year PhD student under the supervision of Alexis Saurin (Université Paris Cité, CNRS, IRIF, INRIA). To visit me: At IRIF, in office 3026. To email me: esaie.bauer@irif dot fr I'm co-organising the INRIA team Picube's seminar: Formath. Formath is a seminar about proof assistants and formalization. I'm also co-organising the Non-permanent members’ seminar. Research I'm interested in proof theory and its link with programming languages. Currently, I'm interested in linear logic and infinite proof theory for various logic. Published articles Super Exponentials in Linear Logic, with Olivier Laurent, Linearity - TLLA 20 - paper Following the idea of Subexponential Linear Logic and Stratified Bounded Linear Logic, we propose a new parameterized version of Linear Logic which subsumes other systems like ELL, LLL or SLL, by including variants of the exponential rules. We call this system Superexponential Linear Logic (superLL). Assuming some appropriate constraints on the parameters of superLL, we give a generic proof of cut elimination. This implies that each variant of Linear Logic which appears as a valid instance of superLL also satisfies cut elimination. Chiralités et exponentielles: un peu de différentiation, with Marie Kerjean, JFLA 2020 (national conference) - paper. Nous donnons une sémantique catégorique à la logique linéaire différentielle finitaire et polarisée. Cette axiomatique donne un cadre à des modèles polarisés précédemment mis à jour dans les espaces vectoriels topologiques. Elle s'appuie sur la notion de chiralités et les modèles non-polarisés de la logique linéaire différentielle munis d'un biproduit. Workshops Cut-elimination for the circular modal μ-calculus: the benefits of linearity, with Alexis Saurin, FICS 2024 - abstract We prove a cut-elimination theorem for the circular modal μ-calculus. More precisely, we establish weak infinitary normalization of a cut-elimination procedure for the non-wellfounded system μLK∞ ◻, using methods from linear logic and its exponential modalities. When sequents are sets of formulas, we obtain weak normalization for the circular modal μ-calculus by coupling cut-elimination with regularization. Provability of Functionnal Reactive Programming type system, with Alexis Saurin - 2021 Workshop on Proof Theory and its Applications -abstract Preprints Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue, with Alexis Saurin - long version The aim of this paper is twofold: contributing to the non-wellfounded and circular proof-theory of the modal mu-calculus and to that of extensions of linear logic with fixed points. Contrarily to Girard's linear logic which is equipped with a rich proof theory, Kozen's modal mu-calculus has an underdeveloped one: for instance the modal mu-calculus is lacking a proper syntactic cut-elimination theorem. A strategy to prove the cut-elimination theorem for the modal mu-calculus is to prove cut-elimination for a “linear translation” of the modal mu-calculus (that is define a translation of the statements and proofs of the modal mu-calculus into a linear sequent calculus) and to deduce the desired cut-elimination results as corollaries. While designing this linear translation, we come up with a sequent calculus exhibiting several modalities (or exponentials). It happens that the literature of linear logic offers tools to manage such calculi, for instance subexponentials by Nigam and Miller and super exponentials by Bauer and Laurent. We actually extend super exponentials with fixed-points and non-wellfounded proofs (of which the linear decomposition of the modal mu-calculus is an instance) and prove a syntactic cut-elimination theorem for these sequent calculi in the framework of non-wellfounded proof theory. Back to the classical modal mu-calculus, we deduce its cut-elimination theorem from the above results, investigating both non-wellfounded and regular proofs. Presentations Presentation at FICS 2024 - Cut-elimination for the circular modal μ-calculus: the bene ts of linearity - slides Presentation at Formath 2024 - Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue - slides Presentation at Non-permanent members' seminar 2023 - Proof theory in Multiplicative-Additive Linear Logic - slides Presentation at Scalp 2023 - Cut-elimination for modal μ-calculus: exploring the expressivity of μMALL - slides Presentation at SeSTeRce - On the geometry of validity criterion for non-wellfounded proofs - slides Presentation at 2021 Workshop on Proof Theory and its Applications Proof and Society Workshop - Provability of Functionnal Reactive Programming type system - slides Presentation at PPS Curry-Howard Correspondance between Temporal Logic and Reactive Programming - slides