Thèse de doctorat: une étude logique du contrôle.

• La version préliminaire du manuscrit est disponible en 3 formats:

  ---

  • version pdf
  • version ps
  • version ps.gz

  ---

• La soutenance aura lieu le 30 septembre 2008 à 14H30 dans l'amphithéâtre Arago, à l'École Polytechnique devant le jury composé de:
  • Pierre-Louis Curien
  • Olivier Danvy
  • François Fages
  • Jean-Yves Girard
  • Olivier Laurent
  • Dale Miller
  • Luke Ong
  • Simona Ronchi della Rocca
  Président du jury: Jean-Yves Girard
  Rapporteurs: Pierre-Louis Curien, Olivier Danvy, Simona Ronchi della Rocca
  Directeur de thèse: Dale Miller
  

  ---

• Résumé de la thèse en anglais (english summary)

---

Pour venir à l'École Polytechnique:

• Indications pour venir à l'X
• Depuis la gare de RER Lozère
• Plan du campus de l'X (l'amphi Arago a le numéro 14, le département d'informatique -- pour le pot -- a le numéro 0)

---

Plan de la thèse:

• Introduction
• Chapitre 1: Notions de théorie de la démonstration
• Chapitre 2: Notions de λ-calcul et de λμ-calcul
• Partie I: Λμ-calcul
• Chapitre 3: Du λμ-calcul au Λμ-calcul
• Chapitre 4: Théorème de Böhm pour le Λμ-calcul
• Chapitre 5: Confluence du Λμ-calcul
• Chapitre 6: Λμ-calcul simplement typé
• Chapitre 7: Une analyse du Λμ-calcul via des réseaux
• Chapitre 8: λμ-calculs, streams et contrôle
• Partie II: Focalisation en logique linéaire
• Chapitre 9: Une preuve modulaire de la focalisation
• Chapitre 10: Multifocalisation
• Partie III: Programmation Ludique
• Chapitre 11: Introduction à la ludique
• Chapitre 12: Vers une programmation ludique: Recherche de preuve interactive
• Conclusion