Separation with Streams in the lambdaµ-calculus. - Alexis Saurin (LICS, 2005)

A Game Semantics for Proof Search: Preliminary Results. - Dale Miller 001; Alexis Saurin (MFPS, 2005)

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. - Dale Miller 001; Alexis Saurin (CSL, 2007)

On the Relations between the Syntactic Theories of lambda-mu-Calculi. - Alexis Saurin (CSL, 2008)

Towards Ludics Programming: Interactive Proof Search. - Alexis Saurin (ICLP, 2008)

Canonical Sequent Proofs via Multi-Focusing. - Kaustuv Chaudhuri; Dale Miller 001; Alexis Saurin (IFIP TCS, 2008)

Standardization and Böhm Trees for Lambdaµ-Calculus. - Alexis Saurin (FLOPS, 2010)

A Hierarchy for Delimited Continuations in Call-by-Name. - Alexis Saurin (FoSSaCS, 2010)

Proof and refutation in MALL as a game. - Olivier Delande; Dale Miller 001; Alexis Saurin (Ann. Pure Appl. Log., 2010)

Intersection Logic in sequent calculus style - Simona Ronchi Della Rocca; Alexis Saurin; Yiorgos Stavrinos; Anastasia Veneti (ITRS, 2010)

From Focalization of Logic to the Logic of Focalization. - Michele Basaldella; Alexis Saurin; Kazushige Terui (MFPS, 2010)

Typing streams in the Λµ-calculus. - Alexis Saurin (ACM Trans. Comput. Log., 2010)

Classical Call-by-Need and Duality. - Zena M. Ariola; Hugo Herbelin; Alexis Saurin (TLCA, 2011)

On the Meaning of Focalization. - Michele Basaldella; Alexis Saurin; Kazushige Terui (PRELUDE Project, 2011)

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. - Zena M. Ariola; Paul Downen; Hugo Herbelin; Keiko Nakata 001; Alexis Saurin (FLOPS, 2012)

Böhm theorem and Böhm trees for the λμ-calculus. - Alexis Saurin (Theor. Comput. Sci., 2012)

Analyse de dépendances et correction des réseaux de preuve. - Marc Bagnol; Amina Doumane; Alexis Saurin (JFLA, 2014)

Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse. - Pierre-Marie Pédrot; Amina Doumane; Alexis Saurin (JFLA, 2014)

Least and Greatest Fixed Points in Ludics. - David Baelde; Amina Doumane; Alexis Saurin (CSL, 2015)

On the Dependencies of Logical Rules. - Marc Bagnol; Amina Doumane; Alexis Saurin (FoSSaCS, 2015)

Infinitary Proof Theory: the Multiplicative Additive Case. - David Baelde; Amina Doumane; Alexis Saurin (CSL, 2016)

Classical By-Need. - Pierre-Marie Pédrot; Alexis Saurin (ESOP, 2016)

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions. - Amina Doumane; David Baelde; Lucca Hirschi; Alexis Saurin (LICS, 2016)

Local Validity for Circular Proofs in Linear Logic with Fixed Points. - Rémi Nollet; Alexis Saurin; Christine Tasson (CSL, 2018)

Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. - Abhishek De 001; Alexis Saurin (TABLEAUX, 2019)

PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points. - Rémi Nollet; Alexis Saurin; Christine Tasson (TABLEAUX, 2019)

The fixed point property and a technique to harness double fixed point combinators. - Giulio Manzonetto; Andrew Polonsky; Alexis Saurin; Jakob Grue Simonsen (J. Log. Comput., 2019)

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. - David Baelde; Amy P. Felty; Gopalan Nadathur; Alexis Saurin (Math. Struct. Comput. Sci., 2019)

Toward a Curry-Howard Equivalence for Linear, Reversible Computation - Work-in-Progress. - Kostia Chardonnet; Alexis Saurin; Benoît Valiron (RC, 2020)

Bouncing threads for infinitary and circular proofs. - David Baelde; Amina Doumane; Denis Kuperberg; Alexis Saurin (CoRR, 2020)

Canonical proof-objects for coinductive programming: infinets with infinitely many cuts. - Abhishek De 001; Luc Pellissier; Alexis Saurin (PPDP, 2021)

Decision Problems for Linear Logic with Least and Greatest Fixed Points. - Anupam Das 002; Abhishek De 001; Alexis Saurin (FSCD, 2022)

Phase Semantics for Linear Logic with Least and Greatest Fixed Points. - Abhishek De 001; Farzad Jafarrahmani; Alexis Saurin (FSTTCS, 2022)

Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs. - David Baelde; Amina Doumane; Denis Kuperberg; Alexis Saurin (LICS, 2022)

A Curry-Howard Correspondence for Linear, Reversible Computation. - Kostia Chardonnet; Alexis Saurin; Benoît Valiron (CSL, 2023)

Comparing Infinitary Systems for Linear Logic with Fixed Points. - Anupam Das 002; Abhishek De 001; Alexis Saurin (FSTTCS, 2023)

A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points. - Alexis Saurin (TABLEAUX, 2023)

The exponential logic of sequentialization. - Aurore Alcolei; Luc Pellissier; Alexis Saurin (MFPS, 2023)

On the cut-elimination of the modal μ-calculus: Linear Logic to the rescue. - Esaïe Bauer; Alexis Saurin (FoSSaCS, 2025)

Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten! - Rémy Cerda; Giulio Manzonetto; Alexis Saurin (FSCD, 2025)

Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. - Alexis Saurin (FSCD, 2025)

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials. - Esaïe Bauer; Alexis Saurin (CoRR, 2025)