Olivier LAURENT

Directeur de Recherche au CNRS

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

Bureau GN1 366 Nord
46, allée d'Italie
69364 Lyon cedex 07

Tel. : 04-72-72-85-03
Fax : 04-72-72-80-80
Mail : olivier.laurent@ens-lyon.fr

• Groupe de travail GeoCal du GDR Informatique Mathématique
• Rencontres mensuelles CHoCoLa (Lyon)

• GaLoP VIII (London, UK : 18 - 19 juillet 2013)
• Summer school on Linear Logic and Geometry of Interaction (Torino, Italie : 27 - 31 août 2013)
• CSL 2013 (Torino, Italie : 2 - 5 septembre 2013)

Enseignement

•  NEW  Cours de Master 2 Linear Logic and Game Semantics (2012-2013) à Lyon (avec Russ Harmer).

Publications

• 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 (long version) (avec Thomas Ehrhard) - I&C 2010 [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]
• Interpreting a Finitary Pi-Calculus in Differential Interaction Nets (short version) (avec Thomas Ehrhard) - CONCUR 07 [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]
• About Translations of Classical Logic into Polarized Linear Logic (avec Laurent Regnier) - LICS 03 [DOI] [BibTeX]
• Slicing polarized additive normalization (avec Lorenzo Tortora de Falco) - LMSLNS 2004 [DOI] [BibTeX]
• Polarized games (long version) - APAL 2004 [DOI] [BibTeX]
• Polarized games (short version) - LICS 02 [DOI] [BibTeX]
• Polarized and Focalized Linear and Classical Proofs (avec Myriam Quatrini et Lorenzo Tortora de Falco) - APAL 2005 [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 property of Linear Logic - 2004 [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]  NEW  l2coq: a shallow embedding of linear logic in Coq - 2012
• [note]  NEW  Sequentialization of Multiplicative Proof Nets - 2013 [BibTeX]
• [note]  NEW  Polynomial Time in Untyped Elementary Linear Logic - 2013 [BibTeX]