Olivier LAURENT

Senior Researcher (Directeur de Recherche) at CNRS

Plume Team
Laboratoire de l'Informatique du Parallélisme (LIP)
ENS Lyon

Office M7 309
46, allée d'Italie
69342 Lyon cedex 07
France

E-mail: olivier.laurent@ens-lyon.fr

Upcoming Events

• PACMAN 2026 (Verona, Italy, June 10-12, 2026)
• TLLA 2026 (Lisboa, Portugal, July 18-19, 2026)
• SD 2026 (Lisboa, Portugal, July 24-25, 2026)
• Proof Society 2026 (Aussois, France, September 7-11, 2026)

• Computer Aided Linear Logic
• Click & coLLecT: an interactive linear logic prover
• Yalla (linear logic in Coq) : version 2.0.7 (for Rocq 9.0-9.2) available (opam package rocq-yalla)
    together with the standard library extension OLlibs

• Rencontres mensuelles CHoCoLa (Lyon)
• Séminaires mensuels Rocq band (Proof Assistant) (Lyon)
   
• Linear Logic wiki ( NEW  PDF version / LaTeX source)
• IRN Logic and Interaction
   
• Projet ReCiProg

• Projet LLipIdO
  • Journée Preuves de logique linéaire sur machine (18/12/18 - ENS Lyon)

Publications

•  NEW  The Logic of Intersection Subtyping - LICS 26 [Rocq] [DOI]
•  NEW  Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints (with Jui-Hsuan Wu) - FSCD 26 [Rocq] [DOI]
•  NEW  YALLA: Yet Another deep embedding of Linear Logic in Rocq - JAR 2026 [Rocq] [DOI] [BibTeX]
•  NEW  Classical Linear Logic is not Conservative over System F - TLLA 26
• Type Isomorphisms for Multiplicative-Additive Linear Logic (with Rémi Di Guardia)
  • long version - LMCS 2025 [DOI] [BibTeX]
  • short version - FSCD 23 [DOI] [BibTeX]
• A Formalization of Multiplicative Proof-Nets in Rocq (with Rémi Di Guardia) - TLLA 25 [Rocq]
• Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic (with Rémi Di Guardia, Lorenzo Tortora de Falco et Lionel Vaux Auclair) - FSCD 25 [DOI] [BibTeX]
• Sequentialization is as fun as bungee jumping (with Rémi Di Guardia, Lorenzo Tortora de Falco et Lionel Vaux Auclair) - TLLA 23
• Bottom-Up Sequentialization of Unit-Free MALL Proof Nets (with Rémi Di Guardia) - Linearity - TLLA 22 [BibTeX]
• An Anti-Locally-Nameless Approach to Formalizing Quantifiers - CPP 21 [Rocq] [DOI] [BibTeX]
• Super Exponentials in Linear Logic (with Esaïe Bauer) - Linearity - TLLA 20 [DOI] [BibTeX]
• Polynomial Time in Untyped Elementary Linear Logic - TCS 2020 [DOI] [BibTeX]
• Resource-Tracking Concurrent Games (with Aurore Alcolei et Pierre Clairambault) - FOSSACS 19 [DOI] [BibTeX]
• Intersection Subtyping with Constructors - ITRS 18 [Rocq] [DOI] [BibTeX]
• Around Classical and Intuitionistic Linear Logics - LICS 18 [Rocq] [DOI] [BibTeX]
• Focusing in Orthologic
  • long version - LMCS 2017[OCaml] [Rocq] [DOI] [BibTeX]
  • short version - FSCD 16 [OCaml] [Rocq] [DOI] [BibTeX]
• Intersection Types with Subtyping by Means of Cut Elimination - FI 2012 [DOI] [BibTeX]
• Intuitionistic Dual-intuitionistic Nets - JLC 2011 [DOI] [BibTeX]
• Game semantics for first-order logic - LMCS 2010 [DOI] [BibTeX]
• Acyclic Solos and Differential Interaction Nets (with Thomas Ehrhard) - LMCS 2010 [DOI] [BibTeX]
• Interpreting a Finitary Pi-Calculus in Differential Interaction Nets (with Thomas Ehrhard)
  • long version - I&C 2010 [DOI] [BibTeX]
  • short version - CONCUR 07 [DOI] [BibTeX]
• An exact correspondence between a typed pi-calculus and polarised proof-nets (with Kohei Honda) - TCS 2010 [DOI] [BibTeX]
• On the categorical semantics of Elementary Linear Logic - TAC 2009 [EE] [BibTeX]
• Quantitative Game Semantics for Linear Logic (with Ugo Dal Lago) - CSL 08 [DOI] [BibTeX]
• Cut Elimination for Monomial MALL Proof Nets (with Roberto Maieli) - LICS 08 [DOI] [BibTeX]
• The anatomy of innocence revisited (with Russ Harmer) - FSTTCS 06 [DOI] [BibTeX]
• Obsessional cliques: a semantic characterization of bounded time complexity (with Lorenzo Tortora de Falco) - LICS 06 [DOI] [BibTeX]
• Classical isomorphisms of types - MSCS 2005 [DOI] [BibTeX]
• Syntax vs. semantics: a polarized approach - TCS 2005 [DOI] [BibTeX]
• Polarized and Focalized Linear and Classical Proofs (with Myriam Quatrini et Lorenzo Tortora de Falco) - APAL 2005 [DOI] [BibTeX]
• Slicing polarized additive normalization (with Lorenzo Tortora de Falco) - LMSLNS 2004 [DOI] [BibTeX]
• Polarized games
  • long version - APAL 2004 [DOI] [BibTeX]
  • short version - LICS 02 [DOI] [BibTeX]
• About Translations of Classical Logic into Polarized Linear Logic (with Laurent Regnier) - LICS 03 [DOI] [BibTeX]
• Polarized proof-nets and lambda-mu calculus - TCS 2003 [DOI] [BibTeX]
• A Token Machine for Full Geometry of Interaction - TLCA 01 [DOI] [BibTeX]
• Polarized Proof-Nets: Proof-Nets for LC - TLCA 99 [DOI] [BibTeX]

Miscellaneous

• [PhD thesis] Étude de la polarisation en logique - 2002 [BibTeX]
• [talk] Polarities in Linear Logic - 2002
• [note] Krivine's abstract machine and the lambda-mu calculus - 2003 [BibTeX]
• [note] On the denotational semantics of the untyped lambda-mu calculus - 2004 [BibTeX]
• [note] A proof of the focalization / focusing property of Linear Logic - 2004 - 2017 [BibTeX]
• [course notes] Sémantique des jeux - 2004
• [talk] Is not not A equal to A? - 2007
• [talk] Sémantique des jeux : de la programmation à la logique - 2008
• [course notes] Théorie de la démonstration - 2008
     (Near-)native English speakers interested in translating these course notes into English, please contact me.
• [HDR thesis] Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire - 2010 [BibTeX]
• [course notes] Réseaux d'interaction - 2010
• [note] A syntactic introduction to intersection types - 2012 [BibTeX]
• [code] l2coq: a shallow embedding of linear logic in Rocq - 2012
• [note] Sequentialization of Multiplicative Proof Nets - 2013 [BibTeX]
• [note] Categories for Me - 2013-2024
• [note] Decorating Proof-Nets with Lambda-Terms - 2015
• [code] Yalla: an LL library for Rocq - 2017-2025
• [talk] Formalizing Linear Logic - 2020
•  NEW  [blog post] On the Canonicity of Linear Logic Connectives - 2026 [PDF]

Some Teaching

• Master 2 course Category Theory for Computer Scientists (partie 2) (2023-2024 et 2024-2025), Lyon.
• Exercise sessions for LL School 2022, Marseille.
• Master 2 course Logical Foundations of Programming Languages (2020-2021 et 2021-2022), Lyon.
• DIU Enseigner l'Informatique au Lycée (bloc 1 & bloc 2) (2018-2019), Lyon
• Master 2 course Implicit Computational Complexity (2015-2016 et 2017-2018), Lyon.
• Master 2 course Linear Logic and Game Semantics (2013-2014 et 2014-2015), Lyon.