====== Alexis Saurin ======


==== Introduction ====

I am a CNRS researcher at IRIF (Institut de Recherche en Informatique fondamentale), member of [[https://www.irif.fr/poles/pps/index|PPS pole]] and [[https://www.irif.fr/equipes/picube/index|Picube Inria team]].

I am in charge, with Esaïe Bauer of the [[https://www.irif.fr/seminaires/picube/index|Formath seminar]], which is the seminar of Picube INRIA team. I am also responsible, with Pierre Clairambault and Chantal Keller, of [[https://www.irif.fr/gt-scalp/index|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é.



==== Research interests ====
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

==== News ====

  * I am organizing [[https://www.irif.fr/users/saurin/FICS2024/index.html|FICS workshop in february 2024]];
  * I am organizing the [[https://www.irif.fr/gt-scalp/journees-2023|2023 annual meeting of SCALP working group, on 27-29 novembre in Orléans]];
  * In september 2023, I presented my recent paper [[https://link.springer.com/chapter/10.1007/978-3-031-43513-3_12|on cut-elimination for full non-wellfounded linear logic with fixed-points]] published in TABLEAU 23. A long version is [[https://hal.science/hal-04169137|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;


/* 
==== Some talks ====

  * 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
  * An invited talk at the Virtual Proof Theory seminar
*/
==== Publications ====

You can find an updated [[https://dblp.org/pid/19/1889.html|list of my publications on DBLP]].

==== Teaching ====

This semester, I am 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)]]

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

  * [[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2023|Second-order quantification and fixed points in logic (SOFIX)]]

==== Students and post-docs ====

== Current PhD student: ==
  * Esaïe Bauer

== Former PhD students: ==
  * Piere-Marie Pédrot
  * Amina Doumane
  * Rémi Nollet
  * Abhishek De
  * Kostia Chardonnet
  * Farzad Jafarrahmani

== Post-doc: == 
  * Aurore Alcoléi

====  ====