| 2026 | CSL | A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. | Alexis Saurin, Esae Bauer |
| 2026 | ITP | Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation. | Meven Lennon-Bertrand, Alexis Saurin |
| 2026 | MFCS | Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs. | Rmy Cerda, Alexis Saurin |
| 2025 | FOSSACS | On the cut-elimination of the modal μ-calculus: Linear Logic to the rescue. | Esae Bauer, Alexis Saurin |
| 2025 | FSCD | Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten! | Rmy Cerda, Giulio Manzonetto, Alexis Saurin |
| 2025 | FSCD | Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. | Alexis Saurin |
| 2025 | LICS | On the denotation of circular and non-wellfounded proofs in linear logic with fixed points. | Thomas Ehrhard, Farzad Jafarrahmani, Alexis Saurin |
| 2023 | CSL | A Curry-Howard Correspondence for Linear, Reversible Computation. | Kostia Chardonnet, Alexis Saurin, Benot Valiron |
| 2023 | TABLEAUX | A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points. | Alexis Saurin |
| 2022 | FSCD | Decision Problems for Linear Logic with Least and Greatest Fixed Points. | Anupam Das, Abhishek De, Alexis Saurin |
| 2022 | LICS | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs. | David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin |
| 2021 | PPDP | Canonical proof-objects for coinductive programming: infinets with infinitely many cuts. | Abhishek De, Luc Pellissier, Alexis Saurin |
| 2020 | RC | Toward a Curry-Howard Equivalence for Linear, Reversible Computation - Work-in-Progress. | Kostia Chardonnet, Alexis Saurin, Benot Valiron |
| 2019 | TABLEAUX | Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. | Abhishek De, Alexis Saurin |
| 2019 | TABLEAUX | PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points. | Rmi Nollet, Alexis Saurin, Christine Tasson |
| 2018 | CSL | Local Validity for Circular Proofs in Linear Logic with Fixed Points. | Rmi Nollet, Alexis Saurin, Christine Tasson |
| 2016 | CSL | Infinitary Proof Theory: the Multiplicative Additive Case. | David Baelde, Amina Doumane, Alexis Saurin |
| 2016 | ESOP | Classical By-Need. | Pierre-Marie Pdrot, Alexis Saurin |
| 2016 | LICS | Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Bchi inclusions. | Amina Doumane, David Baelde, Lucca Hirschi, Alexis Saurin |
| 2015 | CSL | Least and Greatest Fixed Points in Ludics. | David Baelde, Amina Doumane, Alexis Saurin |
| 2015 | FOSSACS | On the Dependencies of Logical Rules. | Marc Bagnol, Amina Doumane, Alexis Saurin |
| 2012 | FLOPS | Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. | Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin |
| 2010 | FLOPS | Standardization and Bhm Trees for Lambda | Alexis Saurin |
| 2010 | FOSSACS | A Hierarchy for Delimited Continuations in Call-by-Name. | Alexis Saurin |
| 2008 | CSL | On the Relations between the Syntactic Theories of lambda-mu-Calculi. | Alexis Saurin |
| 2008 | ICLP | Towards Ludics Programming: Interactive Proof Search. | Alexis Saurin |
| 2007 | CSL | From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. | Dale Miller, Alexis Saurin |
| 2005 | LICS | Separation with Streams in the lambda-calculus. | Alexis Saurin |