[[https://www.irif.fr/_media/users/saurin/pub/cut_elim_modal_draft.pdf|Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue]], with Esaïe Bauer, draft, version of january 2024
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 superexponentials
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.
[[https://hal.science/hal-03655737v1|Polarized linear logic with fixpoints]], with Thomas Ehrhard & Farzad Jafarrahmani, draft 2022
We introduce and study µLLP, which can be viewed both as an extension of Laurent's Polarized Linear Logic, LLP, with least and greatest fixpoints, and as a polarized version of Baelde's Linear Logic with fixpoints (µMALL and µLL). We take advantage of the implicit structural rules of µLLP to introduce a term syntax for this language, in the spirit of the classical lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint introduced by Ehrhard and Jafarrahmani. We prove an adequacy result for µLLP between these operational and denotational semantics, from which we derive a normalization property for µLLP thanks to the properties of the totality interpretation.
==== Teaching ====
During the fall semester 2023-24, I have been teaching at Master LMFI (second year master in mathematical logic and foundations of computer science) at Université Paris Cité.
* [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023|Course on functional programming and formal proofs in Coq (PF2)]]
During the second semester 2023-24, I am teaching with Thomas Colcombet the course on
* [[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2024|Second-order quantification and fixed points in logic (SOFIX)]]
In the previous years, I have mostly been teaching in M2 LMFI (Cours fondamental de logique-théorie de la démonstration; Outils classiques pour la corespondance preuves-programmes; logique linéaire; lambda-calcul et preuves) but also in the Programming M2 (computer labs in the course of Adrien Guatto on synchronous programming) or in L1 (IP1, which is the first introductory course on programming for undergraduate studients).
I also taught in Centre pénitentiaire de Fresnes and Maison d'arrêt de Paris la Santé as a member of the teaching staff of //Section des étudiants empêchés// and I organized some "math club" in the above two prisons well as in Centre pénitentiaire sud-francilien (in the QCD of Réau). Most of my teaching activities were in fact part of voluntary social work as a member of GENEPI (including one year of "civil service" during my PhD studies where I lead this student NGO which does not exist anymore) when I was a student and then as a volunteer in FARAPEJ, in Mathématiques en liberté, and in Champ Libre.
==== Students and post-docs ====
== Current PhD student: ==
* [[https://www.irif.fr/users/ebauer/index|Esaïe Bauer]]
== Former PhD students: ==
* Farzad Jafarrahmani ([[https://www.theses.fr/s230580|defended january 2023]], co-advised with Thomas Ehrhard), currently post-doc in LIP6 ([[https://drive.google.com/file/d/1o9kLi14VDjRb1N2TTfF1WzwG5e25N1xK/view?usp=sharing|manuscript]], [[https://sites.google.com/site/farzadjafarrahmani/|webpage]])
* Kostia Chardonnet ([[https://www.theses.fr/2023UPASG005|defended january 2023]], co-advised with Benoît Valiron), currently post-doc in Bologna ([[https://www.theses.fr/2023UPASG005|manuscript]], [[https://www.lri.fr/~chardonnet/|webpage]])
* Abhishek De ([[https://www.theses.fr/2022UNIP7128|defended december 2022]]), currently post-doc in Birmingham ([[https://www.theses.fr/2022UNIP7128|manuscript]])
* Rémi Nollet (defended summer 2021, co-advised with Christine Tasson), professeur de CPGE ([[https://theses.fr/2021UNIP7100|manuscrit]])
* Amina Doumane ([[https://www.theses.fr/2017USPCC123|defended june 2017]], co-advised with David Baelde), CNRS researcher ([[https://www.theses.fr/2017USPCC123|manuscript]], [[https://perso.ens-lyon.fr/amina.doumane/|webpage]])
* Pierre-Marie Pédrot ([[https://www.theses.fr/2015USPCC240|defended september 2015]], co-advised with Hugo Herbelin), INRIA researcher ([[https://www.pédrot.fr/articles/thesis.pdf|manuscript]], [[https://www.pédrot.fr|webpage]])
== Former Post-doc: ==
* Aurore Alcoléi (jan 2022 - june 2023)
* Luc Pellissier (dec 2018 - dec 2019)
* Andrew Polonsky (jan 2016 - december 2017)
* Guilhem Jaber (dec 2015 - dec 2016)
== Former Master Students: ==
Adrien Shalit,
Esaïe Bauer,
Ikram Cherrigui,
Lucien David,
Kostia Chardonnet,
Rémi Nollet,
Pablo Donato,
Xavier Onfroy,
Paul Fermé,
Amina Doumane,
Paul Downen,
Fanny Hé,
Simon Lunel,
Luke Maurer
==== Contact informations ====
{{page>inc&noheader&nofooter}}