Olivier LAURENT Chargé de Recherche

CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE UNIVERSITE PARIS VII DENIS DIDEROT

• Publications
• Mémoires
• Exposés
• Notes
• LaTeX

Publications

Logique classique et réseaux de preuve

• Polarized Proof-Nets: Proof-Nets for LC (extended abstract) - 1999.
  In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications (TLCA '99), volume 1581 of LNCS, pages 213-227. © Springer-Verlag. Avril 1999.
  version ps.gz - 15 pages - (bibtex)

• Polarized proof-nets and lambda-mu calculus - 2003.
  Theoretical Computer Science (TCS), 290(1):161-188. Janvier 2003.
  version ps.gz - 25 pages - (bibtex)

• About Translations of Classical Logic into Polarized Linear Logic (avec Laurent Regnier) - 2003.
  Eighteenth annual IEEE symposium on Logic In Computer Science (LICS '03), pages 11-20. © IEEE Computer Society. Juin 2003.
  version ps.gz - 10 pages - (bibtex)

• Polarized and Focalized Linear and Classical Proofs (avec Myriam Quatrini et Lorenzo Tortora de Falco) - 2005.
  Annals of Pure and Applied Logic (APAL), 134(2-3):217-264. Juillet 2005.
  version ps.gz - 56 pages - (bibtex)

Connecteurs additifs en logique linéaire

• A Token Machine for Full Geometry of Interaction (extended abstract) - 2001.
  In Samson Abramsky, editor, Typed Lambda Calculi and Applications (TLCA '01), volume 2044 of LNCS, pages 283-297. © Springer-Verlag. Mai 2001.
  version ps.gz - 15 pages - (bibtex)

• Slicing polarized additive normalization (avec Lorenzo Tortora de Falco) - 2004.
  Linear Logic in Computer Science (London Mathematical Society Lecture Notes Series 316 - CUP), pages 247-282. Novembre 2004.
  version ps.gz - 36 pages - (bibtex)

• Cut Elimination for Monomial MALL Proof Nets (avec Roberto Maieli) - 2008.
  Twenty-Third annual IEEE symposium on Logic In Computer Science (LICS '08), pages 486-497. © IEEE Computer Society. Juin 2008.
  version ps.gz - 12 pages - (bibtex)

Sémantique des jeux

• Polarized games - 2002-2004.

  • Seventeenth annual IEEE symposium on Logic In Computer Science (LICS '02), pages 265-274. © IEEE Computer Society. Juillet 2002.
    Extended abstract: version ps.gz - 10 pages - (bibtex)

  • Annals of Pure and Applied Logic (APAL), 130(1-3):79-123. Décembre 2004.
    Special issue "LICS '02".
    Journal version: version ps.gz - 40 pages - (bibtex)

• Syntax vs. semantics: a polarized approach - 2005.
  Theoretical Computer Science (TCS), 343(1-2):177-206. Octobre 2005.
  Game Theory Meets Theoretical Computer Science.
  version ps.gz - 31 pages - (bibtex)
  

• Classical isomorphisms of types - 2005.
  Mathematical Structures in Computer Science (MSCS), 15(5):969-1004. Octobre 2005.
  Isomorphisms of Types.
  version ps.gz - 37 pages - (bibtex)
  

• The anatomy of innocence revisited (avec Russ Harmer) - 2006.
  In S. Arun-Kumar and Naveen Garg, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS '06), volume 4337 of LNCS, pages 224-235. © Springer-Verlag. Décembre 2006.
  version pdf - 12 pages - (bibtex)

Complexité implicite

• Obsessional cliques: a semantic characterization of bounded time complexity (avec Lorenzo Tortora de Falco) - 2006.
  Twenty-first annual IEEE symposium on Logic In Computer Science (LICS '06), pages 179-188. © IEEE Computer Society. Août 2006.
  version ps.gz (avec annexes) - 14 pages - (bibtex)

• Quantitative Game Semantics for Linear Logic (avec Ugo Dal Lago) - 2008.

  • Prépublication électronique de PPS : HAL  hal-00270933. Avril 2008.
    Long version: dépôt HAL - 21 pages - (bibtex)
    

  • In Michael Kaminski and Simone Martini, editors, Computer Science Logic (CSL '08), volume 5213 of LNCS, pages 230-245. © Springer-Verlag. Septembre 2008.
    Extended abstract: version ps.gz - 15 pages - (bibtex)

• On the categorical semantics of Elementary Linear Logic - 2008.
  Soumis. Juin 2008.
  version ps.gz - 32 pages - (bibtex)
  

Concurrence et réseaux

• Embedding the Finitary Pi-Calculus in Differential Interaction Nets (avec Thomas Ehrhard) - 2006.
  3rd International Workshop on Higher-Order Rewriting (HOR '06). Août 2006.
  version ps.gz - 7 pages - (bibtex)

• Interpreting a Finitary Pi-Calculus in Differential Interaction Nets (avec Thomas Ehrhard) - 2007-2008.

  • In Luis Caires and Vasco T. Vasconcelos, editors, Concurrency Theory (CONCUR '07), volume 4703 of LNCS, pages 333-348. © Springer-Verlag. Septembre 2007.
    Extended abstract: version ps.gz - 15 pages - (bibtex)

  • Soumis. Avril 2008.
    Journal version: version pdf - 40 pages - (bibtex)

Mémoires

• Réseaux de preuve polarisés : des réseaux pour LC.
  (Polarized Proof-Nets: Proof-Nets for LC.)
  Mémoire du DEA de Logique Mathématique et Fondements de l'Informatique sous la direction de Laurent Regnier. Septembre 1998.
  version ps.gz (en français) - 23 pages - (bibtex)

• Étude de la polarisation en logique.
  (A study of polarization in logic.)
  Thèse de Doctorat sous la direction de Jean-Yves Girard et Laurent Regnier. Institut de Mathématiques de Luminy - Université Aix-Marseille II. Mars 2002.
  version ps.gz (en français) - 234 pages - résumé abstract (bibtex)

Exposés

• Polarities in Linear Logic.
  Linear Logic workshop (LL 2002), du 25 au 26 juillet 2002 à Copenhagen, suite à LICS '02 dans le cadre de FLoC '02.
  version ps.gz - 22 pages.

• Is not not A equal to A?
  Journées Jean-Yves Girard du 10 au 12 septembre 2007 à Paris.
  version pdf - 45 pages.

Notes

Vulgarisation superflue à l'usage de l'élite et des bien nantis

• Interprétation calculatoire de la logique classique : lambda-mu calcul et machine de Krivine.
  (Krivine's abstract machine and the lambda-mu calculus.)

  • Notes d'un exposé introductif parues dans les prépublications électroniques de PPS : PPS//02/09//n°6 (ln). Septembre 2002.
    Version française (plus ancienne) : version ps.gz (en français) - 15 pages.

  • Version anglaise (légèrement modifiée) des notes précédentes. Septembre 2003.
    Version anglaise (plus récente) : version ps.gz - 22 pages.

• A proof of the focalization property of Linear Logic.
  version ps.gz - 17 pages (version 05/05/04).

• Intersection types with subtyping by means of cut-elimination.
  version ps.gz - 17 pages (version 11/01/05).
  L'élimination des coupures utilisée dans cette note est prouvée en Coq.

Notes de cours

• Éléments de théorie de la démonstration.
  version ps.gz (en français) - 18 pages (version 1999).

• Théorie de la démonstration. (notes du cours de théorie de la démonstration du Master Logique Mathématique et Fondements de l'Informatique)
  version pdf (en français) - 166 pages (version 02/04/08).

• Sémantique des jeux. (notes du cours de sémantique des jeux du DEA de Programmation)
  version ps.gz (en français) - 43 pages (version 2004).

LaTeX

J'utilise et je vous recommande :

• Pour les preuves formelles : bussproofs de Sam Buss.
• Pour les caractères de Logique Linéaire : cmll (sources et documentation) d'Emmanuel Beffara.

Je remercie au passage les auteurs pour m'avoir grandement simplifié la rédaction de la plupart des articles ci-dessus.

L'éthique c'est bien, il en faut... mais c'est un peu comme la logique : c'est trop simple pour intervenir dans les rapports humains...

M. Larcenet

Il faut faire des enfants, Marco, ça fait de nous des hommes meilleurs...

M. Larcenet