Olivier LAURENT Chargé de Recherche

CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE UNIVERSITE PARIS VII DENIS DIDEROT

Publications

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)

• 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)

Géométrie de l'interaction

• 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)

Logique classique (analyse linéaire)

• 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)

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, special issue "LICS '02". Décembre 2004.
    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)
  

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. 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. Institut de Mathématiques de Luminy - Université Aix-Marseille II. Mars 2002.
  version ps.gz (en français) - 234 pages - résumé abstract (bibtex)

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 ps.gz version pdf (en français) - 162 pages (version 2005).

• 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.