|
Responsables : Delia Kesner et Dale Miller
Le cours commence le lundi 12 septembre!
Introduction à la Logique Linéaire et Recherche de preuve (12h, Dale Miller : 12/09/23, 19/09/23, 26/10/23, 03/10/23)
Interprétation calculatoire des séquents (12h, Delia Kesner: 10/10/23, 17/10/23, 24/10/23, 31/10/23)
Lambda Calcul, types et modèles (12h, Giulio Manzonetto: 5/12/23, 12/12/23, 9/1/24, 16/1/24)
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)
Partie I (Miller): Date 21 Novembre, de 17h à 20h, salle 1021, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
Partie I (Kesner): Date 21 Novembre, de 17h à 20h, salle 1021, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
Partie II (Manzonetto): Date 5 Mars, de 16h à 19h, salle 1009, SG (tous documents autorisés, ordinateurs et téléphones portables interdits)
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.
Introduction à la Logique Linéaire (notes du cours 2016/2017 de R. di Cosmo) : en anglais
-
Pour les réseaux de preuve de la Logique Linéaire: An introduction to proof-nets de O. Laurent en anglais
Correspondance de Curry-Howard en Logique Classique : en anglais
Recherche de preuve et calcul logique : en anglais
- 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).
B. Accattoli |
CR |
INRIA |
LIX |
D. Kesner |
PU |
Univ. Paris Cité |
IRIF |
G. Manzonetto |
PU |
Univ. Paris Cité |
IRIF |
D. Miller |
DR |
INRIA |
Saclay |
|