Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-1 [2018/10/03 09:21]
pagani [Supports de cours]
cours:c-2-1 [2019/10/15 19:25] (current)
kesner [Dates des examens pour 2019-2020]
Line 4: Line 4:
 Responsables : Delia Kesner et Dale Miller Responsables : Delia Kesner et Dale Miller
  
-==== Plan du cours et intervenants prévus pour 2018-2019  ====+==== Plan du cours et intervenants prévus pour 2019-2020  ====
  
 Le cours commence le **vendredi 14 septembre**! Le cours commence le **vendredi 14 septembre**!
  
-  -  Introduction à la Logique Linéaire (12h, Michele Pagani : **14/921/928/09, 5/10**)  +  -  Introduction à la Logique Linéaire (12h, Michele Pagani : **16/0923/0930/09, 07/10**)  
-  -  Interprétation calculatoire des séquents (12h, Delia Kesner: **12/10, 19/10, 26/10, 2/11**)  +  -  Interprétation calculatoire des séquents (12h, Delia Kesner: **14/10, 21/10, 28/10, 04/11**)  
-  -  Stratégies d’evaluation, machines abstraites, et modeles de couts (12h, Beniamino Accattoli: **21/12, 11/118/125/1**) +  -  Stratégies d’evaluation, machines abstraites, et modeles de couts (12h, Beniamino Accattoli: **09/12, 16/1206/0113/01**) 
-  -  Recherche de preuve et calcul logique (12h, Dale Miller: **1/28/215/222/2**) +  -  Recherche de preuve et calcul logique (12h, Dale Miller: **20/0127/0103/0210/02**) 
  
-==== Dates des examens pour 2018-2019  ====+==== Dates des examens pour 2019-2020  ====
  
-  -  Partie  I: **TBA**, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits) +  -  Partie  I: 18/11/2019, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits) 
-  -  Partie II: **TBA**, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits)+  -  Partie II: 02/03/2019, aux horaires du cours (tous documents autorisés, ordinateurs et téléphones portables interdits)
 ==== Motivations et objectifs ==== ==== Motivations et objectifs ====
  
Line 49: Line 49:
 <li> Interprétation calculatoire des séquents: <li> Interprétation calculatoire des séquents:
 <ul> <ul>
-<li> Différentes interprétations calculatoires de la déduction +<li> Logique Linéaire Multiplicative Exponentielle (MELL).</li> 
- naturelle intuitionniste.</li> +<li> Réseaux de preuves pour MELL. </li> 
-<li> Calcul de resources. </li> +<li> Calculs avec substitutions explicites (syntaxe, sémantique, propriétés).</li> 
-<li> Discussion sur la notion de réduction associée  +<li> Traduction du lambda-calcul avec substitutions explicites dans les réseaux de
-   aux  réseaux de preuves de MELL.</li> +
-<li> Traduction du lambda-calcul dans les réseaux de+
  preuves de MELL. </li>  preuves de MELL. </li>
-<li> Différentes interprétations calculatoires du calcul de Gentzen 
-   intuitionniste. </li> 
 <li> Introduction aux types intersection et leur relation avec la logique linéare. </li> <li> Introduction aux types intersection et leur relation avec la logique linéare. </li>
 </ul> </ul>
Line 96: Line 92:
 ==== Langues du cours ==== ==== Langues du cours ====
  
-Les parties 1 et 2 du cours seront dispens&eacute;es en Français; les parties 3 et 4 le seront en Anglais. Le sujet d'examen sera en français et/ou en anglais. +Le cours sera dispens&eacute;en Anglais. 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.+Les étudiants pourront rédiger leur examen en français et/ou anglais.
  
  
Line 105: Line 101:
   - LL wiki : [[http://llwiki.ens-lyon.fr/mediawiki/index.php/Main_Page|en anglais]]   - LL wiki : [[http://llwiki.ens-lyon.fr/mediawiki/index.php/Main_Page|en anglais]]
   - Pour les réseaux de preuve de la Logique Linéaire: An introduction to proof-nets de O. Laurent [[http://perso.ens-lyon.fr/olivier.laurent/pn16.pdf|en anglais]]   - Pour les réseaux de preuve de la Logique Linéaire: An introduction to proof-nets de O. Laurent [[http://perso.ens-lyon.fr/olivier.laurent/pn16.pdf|en anglais]]
-  -  Interprétation calculatoire des séquents : [[http://www.pps.jussieu.fr/~kesner/enseignement/mpri/ll/|en anglais]] 
   -  Correspondance de Curry-Howard en Logique Classique : [[http://www.lix.polytechnique.fr/~lengrand/Work/Teaching/MPRI/|en anglais]]   -  Correspondance de Curry-Howard en Logique Classique : [[http://www.lix.polytechnique.fr/~lengrand/Work/Teaching/MPRI/|en anglais]]
   -  Recherche de preuve et calcul logique : [[http://www.lix.polytechnique.fr/Labo/Dale.Miller/mpri/|en anglais]]   -  Recherche de preuve et calcul logique : [[http://www.lix.polytechnique.fr/Labo/Dale.Miller/mpri/|en anglais]]
Line 120: Line 115:
 ==== Cours liés ==== ==== Cours liés ====
  
-Si vous suivez ce cours, on vous recommande de suivre aussi le cours 2-2. Pour la cultureles cours 2-3, 2-4-et  2-7-1 sont proches aussi.+Si vous suivez ce cours, on vous recommande de suivre aussi le cours 2-2, 2-4, 2-7-et  2-7-2.
  
 ==== Bibliographie ==== ==== Bibliographie ====
 
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