Olivier LAURENT

Directeur de Recherche au CNRS

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

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

Tel. : 04-72-72-83-52
Fax : 04-72-72-80-80
Mail : olivier.laurent@ens-lyon.fr

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

• Rencontres mensuelles CHoCoLa (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

• Type Isomorphisms for Multiplicative-Additive Linear Logic (avec Rémi Di Guardia)
  •  NEW  long version - to appear in LMCS
  • short version - FSCD 23 [DOI] [BibTeX]
•  NEW  A Formalization of Multiplicative Proof-Nets in Rocq (avec Rémi Di Guardia) - TLLA 25 [Rocq]
•  NEW  Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic (avec Rémi Di Guardia, Lorenzo Tortora de Falco et Lionel Vaux Auclair) - FSCD 25 [DOI]
• Sequentialization is as fun as bungee jumping (avec Rémi Di Guardia, Lorenzo Tortora de Falco et Lionel Vaux Auclair) - TLLA 23
• Bottom-Up Sequentialization of Unit-Free MALL Proof Nets (avec 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 (avec Esaïe Bauer) - Linearity - TLLA 20 [DOI] [BibTeX]
• Polynomial Time in Untyped Elementary Linear Logic - TCS 2020 [DOI] [BibTeX]
• Resource-Tracking Concurrent Games (avec 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 (avec Thomas Ehrhard) - LMCS 2010 [DOI] [BibTeX]
• Interpreting a Finitary Pi-Calculus in Differential Interaction Nets (avec 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 (avec Kohei Honda) - TCS 2010 [DOI] [BibTeX]
• On the categorical semantics of Elementary Linear Logic - TAC 2009 [EE] [BibTeX]
• Quantitative Game Semantics for Linear Logic (avec Ugo Dal Lago) - CSL 08 [DOI] [BibTeX]
• Cut Elimination for Monomial MALL Proof Nets (avec Roberto Maieli) - LICS 08 [DOI] [BibTeX]
• The anatomy of innocence revisited (avec Russ Harmer) - FSTTCS 06 [DOI] [BibTeX]
• Obsessional cliques: a semantic characterization of bounded time complexity (avec 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 (avec Myriam Quatrini et Lorenzo Tortora de Falco) - APAL 2005 [DOI] [BibTeX]
• Slicing polarized additive normalization (avec 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 (avec 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]

Divers

• [thèse] Étude de la polarisation en logique - 2002 [BibTeX]
• [exposé] 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]
• [cours] Sémantique des jeux - 2004
• [exposé] Is not not A equal to A? - 2007
• [exposé] Sémantique des jeux : de la programmation à la logique - 2008
• [cours] Théorie de la démonstration - 2008
     (Near-)native English speakers interested in translating these course notes into English, please contact me.
• [hdr] Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire - 2010 [BibTeX]
• [cours] 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
• [exposé] Formalizing Linear Logic - 2020

Enseignement récent

• Cours de Master 2 Category Theory for Computer Scientists (partie 2) (2023-2024 et 2024-2025) à Lyon.
• Exercise sessions for LL School 2022 à Marseille.
• Cours de Master 2 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
• Cours de Master 2 Implicit Computational Complexity (2015-2016 et 2017-2018) à Lyon.
• Cours de Master 2 Linear Logic and Game Semantics (2013-2014 et 2014-2015) à Lyon.