Responsables : Delia Kesner et Dale Miller

Le cours commence le lundi 12 septembre!

1. Introduction à la Logique Linéaire et Recherche de preuve (12h, Dale Miller : 12/09/23, 19/09/23, 26/10/23, 03/10/23)
2. Interprétation calculatoire des séquents (12h, Delia Kesner: 10/10/23, 17/10/23, 24/10/23, 31/10/23)
3. Lambda Calcul, types et modèles (12h, Giulio Manzonetto: 5/12/23, 12/12/23, 9/1/24, 16/1/24)
4. Stratégies d’evaluation, machines abstraites, et modèles de couts (12h, Beniamino Accattoli: 23/1/24, 30/1/24, 6/2/24, 13/2/24)

1. Partie I (Miller): Date 21 Novembre, de 17h à 20h, salle 1021, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
2. Partie I (Kesner): Date 21 Novembre, de 17h à 20h, salle 1021, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
3. Partie II (Manzonetto): Date 5 Mars, de 16h à 19h, salle 1009, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
4. Partie II (Accattoli): Date 5 Mars, de 16h à 19h, salle 1009, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)-

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.

• Introduction à la Logique Linéaire et recherche de preuves
  • Du calcul des séquents classique à la logique linéaire.
  • Pouvoir d'expression: LJ et LK dans la logique linéaire.
  • 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éair.
    • Chaînage avant, chaînage arrière.
    • Recherche de preuves et calcul logique
    • La logique linéaire comme meta-logique: spécification et raisonnement.
  • Les outils pour l'interprétation calculatoire des séquents:
    • Logique Linéaire Multiplicative Exponentielle (MELL).
    • Réseaux de preuves pour MELL.
    • Critères de correction.
    • Réduction dans les réseaux et théorèmes de normalisation.
  • L'interprétation calculatoire des séquents:
    • 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.
  • Modèles de couts, machines abstraites, et stratégies d’evaluation :
  • Modèles de coûts et explosion de la taille, propriété du sous-terme.
  • Machines abstraites et leur analyse de complexité.
  • Analyse de la Milner Abstract Machine (MAM).
  • Le calcul des substitutions linéaires (LSC).
  • Le passage par valeur, le passage par nécessité, machines par valeurs et par nécessité.
  • Types intersection et temps de calcul.

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.

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

• Beniamino Accattoli
• Delia Kesner
• Giulio Manzonetto
• Dale Miller

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

Si vous suivez ce cours, on vous recommande de suivre aussi le cours 2-2, 2-4, 2-7-1 et 2-7-2.

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