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

• Polarized and Focalized Linear and Classical Proofs (avec Myriam Quatrini et Lorenzo Tortora de Falco) - 2000.
  Prépublication n°24, Institut de Mathématiques de Luminy (CNRS). Septembre 2000.
  version ps.gz version pdf - 42 pages - (bibtex)
  À paraître dans Annals of Pure and Applied Logic (APAL), 2005.
  version ps.gz - 56 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)

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 - 2003.
  Prépublication électronique de PPS : PPS//03/04//n°17 (pp) et HAL : ccsd-00003759. Mars 2003
  version ps.gz - 31 pages - (bibtex)
  Soumis à la revue Theoretical Computer Science, special issue "Game Theory Meets Theoretical Computer Science".

• Classical isomorphisms of types - 2003.
  Prépublication électronique de PPS : PPS//03/04//n°18 (pp) et HAL : ccsd-00003761. Avril 2003
  version ps.gz - 36 pages - (bibtex)
  Soumis à la revue Mathematical Structures in Computer Science, special issue "Isomorphisms of Types".

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)

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.

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 partielles 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) - 91 pages (version 15/02/05).
  Version en chantier ! tout commentaire est le bienvenu !

• 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

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