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 : Delia Kesner et Dale Miller

Plan du cours et intervenants prévus pour 2019-2020

Le cours commence le vendredi 14 septembre!

  1. Introduction à la Logique Linéaire (12h, Michele Pagani : 16/09, 23/09, 30/09, 07/10)
  2. Interprétation calculatoire des séquents (12h, Delia Kesner: 14/10, 21/10, 28/10, 04/11)
  3. Stratégies d’evaluation, machines abstraites, et modeles de couts (12h, Beniamino Accattoli: 09/12, 16/12, 06/01, 13/01)
  4. Recherche de preuve et calcul logique (12h, Dale Miller: 20/01, 27/01, 03/02, 10/02)

Dates des examens pour 2019-2020

  1. Partie I: 18/11/2019, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits)
  2. Partie II: 02/03/2019, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits)

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

  • 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.
    • Sémantiques des phases des formules de la logique linéaire.
    • Réseaux de preuves et critères de correction.
    • Réduction dans les réseaux et théorèmes de normalisation.
  • Interprétation calculatoire des séquents:
    • Logique Linéaire Multiplicative Exponentielle (MELL).
    • Réseaux de preuves pour MELL.
    • Calculs avec substitutions explicites (syntaxe, sémantique, propriétés).
    • Traduction du lambda-calcul avec substitutions explicites dans les réseaux de preuves de MELL.
    • Introduction aux types intersection et leur relation avec la logique linéare.
  • Stratégies d’evaluation, machines abstraites, et modeles de couts:
    • Le calcul des substitutions linéaires: proprietés de base, réduction linéaire de tête, résidus.
    • Machines abstraites et leur analyse de complexité: modèles de coûts et explosion de la taille, propriété du sousterme.
    • Strategies d’evaluation: le passage par valeur, le passage par nécessité, machines par valeurs et par nécessité.
    • Lien entre logique classique, logique linéaire, et calculs: logique linéaire polarisé, lambda-mu-calcul et sa traduction dans les réseaux de preuve polarisés.
  • Recherche de preuve et calcul logique
    • Principes de la recherche de preuves: contexte, coupures, preuves focalisées, connecteurs asynchrones et synchrones.
    • Conception des langages de programmation logique:
      • 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 et raisonnement.

Langues du cours

Le cours sera dispensée en Anglais. Le sujet d'examen sera en français et/ou en anglais. Les étudiants pourront rédiger leur examen en français et/ou anglais.

Supports de cours

  1. Introduction à la Logique Linéaire (notes du cours 2016/2017 de R. di Cosmo) : en anglais
  2. LL wiki : en anglais
  3. Pour les réseaux de preuve de la Logique Linéaire: An introduction to proof-nets de O. Laurent en anglais
  4. Correspondance de Curry-Howard en Logique Classique : en anglais
  5. Recherche de preuve et calcul logique : en anglais

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, 2-4, 2-7-1 et 2-7-2.

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 [[http://plato.stanford.edu/archives/fall2006/entries/logic-linear/][(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).

Équipe pédagogique

B. Accattoli CR INRIA LIX
D. Kesner PU Paris 7 IRIF
D. Miller DR INRIA Saclay
M. Pagani PU Paris 7 IRIF

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA