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

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 benets 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