Alexis Saurin

I am a CNRS researcher at IRIF (Institut de Recherche en Informatique fondamentale), member of PPS pole and Picube Inria team.

I am in charge, with Esaïe Bauer of the Formath seminar, which is the seminar of Picube INRIA team. I am also responsible, with Pierre Clairambault and Chantal Keller, of chairing the Scalp working group of GDR-IM and organizing its annual meetings.

I am an elected member of the research council and the academic council of the faculty of Science at Université Paris Cité.

My research interests are at the interplay between structural proof theory and the theory of programming, both from a syntactical and semantical perspective. More precisely, I am currently interested in:

• fixed points in logic and programming
• circular and non-wellfounded proofs
• linear logic and computational interpretations of classical and intuitinistic logic
• type theory and in particular inductive and coinductive types
• interactive theorem proving
• proof nets and the logic of correctness criteria
• interactive and denotational semantics of proofs and programs
• lambda-calculus and its classical and infinitary extensions
• focusing

• I am organizing FICS workshop in february 2024;
• I am organizing the 2023 annual meeting of SCALP working group, on 27-29 novembre in Orléans;
• In september 2023, I presented my recent paper on cut-elimination for full non-wellfounded linear logic with fixed-points published in TABLEAU 23. A long version is accessible here;
• I recently gave an invited tutorial at TLLA 2023 in Rome;
• Aurore Alcolei presented our joint paper at MFPS 2023;
• David Baelde presented our paper on circular proofs with Bouncing threads at LICS, during FLOC 2022;
• Kostia Chardonnet presented our paper at CSL 2023;
• Abhishek De presented our paper at FSTTCS 2022;
• I gave an invited talk at the sepcial session on logic in computer science, at Logic colloquium june 2022;
• I gave an invited talk at Strip workshop, in Birmingham, may 2022;

You can find an updated list of my publications on DBLP.

This semester, I am teaching at Master LMFI (second year master in mathematical logic and foundations of computer science) at Université Paris Cité.

• Course on functional programming and formal proofs in Coq (PF2)

Last year, I was teachnig with Thomas Colcombet the course on

• Second-order quantification and fixed points in logic (SOFIX)

• Esaïe Bauer

• Piere-Marie Pédrot
• Amina Doumane
• Rémi Nollet
• Abhishek De
• Kostia Chardonnet
• Farzad Jafarrahmani

• Aurore Alcoléi