Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Logique linéaire et paradigmes logiques du calcul (48h, 6 ECTS)

Responsables : Roberto Di Cosmo et Dale Miller

Plan du cours et intervenants prévus pour 2009-2010

1. Introduction à la Logique Linéaire (12.5h, Roberto Di Cosmo) .
2. Interprétation calculatoire des séquents (12.5h, Delia Kesner) .
3. Recherche de preuve et calcul logique (12.5h, Dale Miller) .
4. Correspondance de Curry-Howard en Classical Logic (12.5h, Stéphane Lengrand) .

Dates des examens pour 2009-2010

1. Partie I: le 20 novembre 2009 aux horaires du cours (tous documents autorisés)

Motivations et objectifs

Une analyse fine des calculs de séquents classiques et intuitionnistes permet de concevoir des logiques plus adaptées aux problèmes de l'informatique et de dévélopper, grâce à la correspondance de Curry-Howard des formalismes intermédiaires entre le λ-calcul et les vrais langages de programmation.

Ce cours a pour but de donner une vision d'ensemble des motivations et des applications d'une de ces logiques, la Logique Linéaire, qui permet une analyse plus fine des processus de démonstration et de calcul, et d'introduire les notions de base des calculs intermédiaires les plus connus. On montrera dans le cours comment ces deux approches se rejoignent, à travers des interprétations calculatoires adaptées.

Ce cours dédie une attention toute particulière aux aspects syntaxiques et calculatoires des formalismes logiques.

Description du cours

Syntaxe et calcul fonctionnel

• Introduction à la Logique Linéaire
  • Du calcul des séquents classique à la logique linéaire.
  • Pouvoir d'expression: LJ et LK dans la logique linéaire.
  • Réseaux de preuves et critères de correction.
  • Réduction dans les réseaux et réduction optimale.
  • Géométrie de l'interaction.
• Interprétation calculatoire des séquents:
  • Différentes interprétations calculatoires de la déduction naturelle intuitionniste.
  • Calcul de resources.
  • Discussion sur la notion de réduction associée aux réseaux de preuves de MELL.
  • Traduction du lambda-calcul dans les réseaux de preuves de MELL.
  • Différentes interprétations calculatoires du calcul de Gentzen intuitionniste.

Recherche de preuve et calcul logique

• Principes de la recherche de preuves
  • le contexte dans les règles d'introduction
  • preuves sans coupures, preuves focalisées
  • connecteurs asynchrones et synchrones
• Conception des langages de programmation logique
  • en logique classique, intuitionniste, et linéaire
  • avec quantification à l'ordre supérieur
  • unification, chaînage avant, chaînage arrière
• La logique linéaire comme meta-logique
  • spécification de la sémantique opérationnelle des langages de programmation
  • comment raisonner sur les spécifications basées sur la recherche de preuves

Correspondance de Curry-Howard en Classical Logic

• Calcul des séquents classique vu comme un système de typage
• notion de continuation
• non-confluence de l'élimination des coupures
• forte normalisation et orthogonalité
• Stratégies d'élimination des coupures:
• restrictions confluentes, appel-par-nom et appel-par-valeur
• traductions par continuations vs. traductions par double négation / A-traduction, etc...
• Extensionalité:
Eta-conversion, axiomes atomiques, invertibilité des règles d'introduction
• Polarisation et focalisation:
• impact sur l'élimination des coupures
• introduction à la réalisabilité classique.

Langues du cours

Les parties 1, 2 et 4 du cours seront dispensées en Français; la partie 3 le sera en Anglais (possibilité de l'Anglais aussi pour la partie 4 si souhaité; à convenir avec les étudiants). Le sujet d'examen sera en français et/ou en anglais. Les étudiants pourront rédiger leur examen en français ou en anglais.

Supports de cours

1. Introduction à la Logique Linéaire : en anglais
2. Interprétation calculatoire des séquents : en anglais
3. Recherche de preuve et calcul logique : en anglais
4. Correspondance de Curry-Howard en Classical Logic : ---^?

Pré-requis

• notions élémentaires de logique et déduction naturelle
• notions élémentaires de programmation logique
• notions élémentaires de lambda calcul et de systèmes de types (types simples, système F)
• notions élémentaires de complexité calculatoire (classes de complexité en temps définies par les machines de Turing)

Cours liés

Si vous suivez ce cours, on vous recommande de suivre aussi le cours 2-2. Pour la culture, les cours 2-3, 2-4-2 et 2-7-1 sont proches aussi.

Bibliographie

• J.Y. Girard, Linear Logic, Theoretical Computer Science 50 (1), 1987.
• J.Y. Girard, Y. Lafont, P. Taylor, Proofs and types, Cambridge University Pres, 1989.
• R. Di Cosmo et D. Miller. – Linear Logic. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
• R. Di Cosmo et D. Kesner. – Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In : Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, pp. 35–46. – Warsaw, Poland, 29 juin- 2 juillet 1997.
• D. Kesner et S. Lengrand. – Resource Operators for lambda-calculus. Information and Computation. 205(4):419-473, 2007.
• A. Asperti et S. Guerrini. – The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1998.
• J.-J. Lévy. Optimal Reductions in the lambda-calculus. In : To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin et J.R. Hindley (eds.), pp. 159-191. Academic Press, 1980.
• S. Guerrini. – Proof nets and the lambda-calculus. In : Linear Logic in Computer Science, T. Ehrhard, P. Ruet, J.-Y. Girard et P. Scott (eds.). Cambridge University Press, 2004.
• A. Asperti et H.G. Mairson – Parallel beta is not elementary recursive. In : Proc. 25-th Annual ACM Symposium on Principles of Programming Languages (POPL '98), Albuquerque, New Mexico. ACM Press, 1998.
• D. Miller. – A Multiple-Conclusion Meta-Logic. Theoretical Computer Science 165(1): 201- 232, 1996.
• D. Miller, G. Nadathur, F. Pfenning, et A. Scedrov. – Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, Vol. 51, 125 – 157 (1991).