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-7-2 [2018/11/06 11:20]
sozeau [Evaluation du module]
cours:c-2-7-2 [2019/09/20 12:03] (current)
barras [Transparents cours et TPs]
Line 4: Line 4:
 Responsable : [[http://www.lix.polytechnique.fr/~barras/|Bruno Barras]] Responsable : [[http://www.lix.polytechnique.fr/~barras/|Bruno Barras]]
  
-==== Informations pratiques pour 2018-2019 ====+==== Informations pratiques pour 2019-2020 ====
  
-  *  Le cours a lieu en salle <del>2036</del> 1004, le jeudi de 8h45 à 11h45+  *  Le cours a lieu en salle 1014, le vendredi de 16h15 à 19h15
   *  Il est nécessaire d'apporter un ordinateur portable sur lequel [[http://coq.inria.fr/download|Coq]] est installé pour les travaux pratiques (version 8.5 ou plus de préférence).   *  Il est nécessaire d'apporter un ordinateur portable sur lequel [[http://coq.inria.fr/download|Coq]] est installé pour les travaux pratiques (version 8.5 ou plus de préférence).
   * Il est demandé un niveau de pratique de Coq minimal. Pour cela, il est conseillé de suivre *une* des méthodes introductives citées plus bas (ou bien le début pour les plus elaborées).   * Il est demandé un niveau de pratique de Coq minimal. Pour cela, il est conseillé de suivre *une* des méthodes introductives citées plus bas (ou bien le début pour les plus elaborées).
-  * <html><span style="color:red;">Nouveauté 2018-2019:</span></html> Le module est passé au 1er semestre: premier cours le 13 septembre. 
  
-==== Intervenants pour 2018-2019 ====+==== Intervenants pour 2019-2020 ====
  
     * [[http://www.lix.polytechnique.fr/~barras|Bruno Barras]] (12h)     * [[http://www.lix.polytechnique.fr/~barras|Bruno Barras]] (12h)
     * [[http://www.pps.univ-paris-diderot.fr/~sozeau/|Matthieu Sozeau]] (12h)     * [[http://www.pps.univ-paris-diderot.fr/~sozeau/|Matthieu Sozeau]] (12h)
-<html><!--  *  [[http://specfun.inria.fr/mahboubi/|Assia Mahboubi]] (12h) --></html> 
- 
  
 ==== Objectifs ==== ==== Objectifs ====
Line 32: Line 29:
 ==== Plan du cours ==== ==== Plan du cours ====
  
-Le corps principal de ce cours est formé de séances de 3h abordant les sujets suivants:+Le corps principal de ce cours est formé de séances de 3h abordant les sujets suivants:
   - Rappels et mise à niveau (2 séances): lambda-calcul, types dépendents, isomorphisme de Curry-Howard, Calcul des Constructions.    - Rappels et mise à niveau (2 séances): lambda-calcul, types dépendents, isomorphisme de Curry-Howard, Calcul des Constructions. 
   - Introduction au Calcul des Constructions Inductives et au système Coq. Du calcul des constructions pur aux constructions inductives.    - Introduction au Calcul des Constructions Inductives et au système Coq. Du calcul des constructions pur aux constructions inductives. 
Line 39: Line 36:
  
  
-Le module se terminera avec séances qui traiteront de points pris dans la liste suivante:+Le module se terminera avec séances qui traiteront de points pris dans la liste suivante:
   - Réalisabilité, extraction de programmes à partir de preuves.   - Réalisabilité, extraction de programmes à partir de preuves.
   - Programmation fonctionnelle : récursion structurelle versus accessibilité, fonctions partielles, définitions co-inductives.   - Programmation fonctionnelle : récursion structurelle versus accessibilité, fonctions partielles, définitions co-inductives.
Line 52: Line 49:
 ==== Evaluation du module ==== ==== Evaluation du module ====
  
-  * Examen écrit, durée 3h. Le 22/11/2018, de 8h45 à 11h45+  * Examen écrit, durée 3h.  
-  * Exercices en Coq à préparer individuellement, à partir de la moitié du cours. Ces exercices consisteront à implanter des définitions ou prouver des lemmes (remettre le fichier source), ou encore expliquer des choix de modélisation (document PDF).+  * 1 Exercice en Coq à préparer individuellement, à partir de la moitié du cours. Cet exercice consistera à implanter des définitions ou prouver des lemmes (remettre le fichier source), et expliquer les choix de modélisation ou difficultés rencontrées (document PDF).
  
 ==== Langues du cours ==== ==== Langues du cours ====
Line 60: Line 57:
 ==== Supports de cours ==== ==== Supports de cours ====
  
-Polycopié "Assistants de Preuves" ([[http://www.lix.polytechnique.fr/~barras/mpri/notes/cours.pdf|PDF]], [[http://www.lix.polytechnique.fr/~barras/mpri/notes/index-2-7-2.html|HTML]]). Attention, ce polycopié est lié à une version antérieure du cours : il ne couvre ainsi pas la totalité de ce qui sera abordé mais traite aussi de sujets +Polycopié "Assistants de Preuves" ([[http://www.lix.polytechnique.fr/~barras/mpri/notes/cours.pdf|PDF]], [[http://www.lix.polytechnique.fr/~barras/mpri/notes/index-2-7-2.html|HTML]]). Attention, ce polycopié est lié à une version antérieure du cours : il ne couvre ainsi pas la totalité de ce qui sera abordé mais traite aussi de sujets qui ne sont pas au programme de cette année.
-qui ne sont pas au programme de cette année.+
  
 ==== Transparents cours et TPs ==== ==== Transparents cours et TPs ====
  
 Cette section se remplira cours après cours... Cette section se remplira cours après cours...
-  * {{:cours:upload:2-7-2-2018-cours1-v2.pdf|Cours 1}}, {{:cours:upload:2-7-2-2018-tp1.pdf|TP 1}}, {{:cours:upload:2-7-2-2018-tp1c.v.txt|corrigé}} +  * {{:cours:upload:2-7-2-2019-cours1.pdf|Cours 1}}, {{:cours:upload:2-7-2-2019-tp1.pdf|TP 1}}, {{:cours:upload:2-7-2-2019-tp1c.v.txt|corrigé}} 
-  * {{:cours:upload:2-7-2-2018-cours2.pdf|Cours 2}}, {{:cours:upload:2-7-2-2018-tp2.pdf|TP 2}}, {{:cours:upload:2-7-2-2018-tp2c.v.txt|corrigé}} + 
-  * {{:cours:upload:2-7-2-2018-cours3.pdf|Cours 3}}, {{:cours:upload:2-7-2-2018-tp3.pdf|TP 3}}, {{:cours:upload:2-7-2-2018-tp3c.v.txt|corrigé}} +
-  * {{:cours:upload:2-7-2-2018-cours4.pdf|Cours 4}}, [[https://www.irif.fr/~sozeau/teaching/MPRI-2-7-2-2018/|Énoncés et Corrigés]]  +
-  * {{:cours:upload:2-7-2-2018-cours5.pdf|Cours 5}}, [[https://www.irif.fr/~sozeau/teaching/MPRI-2-7-2-2018/|Énoncés et Corrigés]]  +
-  * {{:cours:upload:2-7-2-2018-cours6.pdf|Cours 6}}, {{:cours:upload:2-7-2-2018-tp6.pdf|TP 6}} +
-  * {{:cours:upload:2-7-2-2018-cours7.pdf|Cours 7}}, [[https://www.irif.fr/~sozeau/teaching/MPRI-2-7-2-2018/|Énoncés et Corrigés]]  +
-  * {{:cours:upload:2-7-2-2018-cours8.pdf|Cours 8}}, [[https://www.irif.fr/~sozeau/teaching/MPRI-2-7-2-2018/|Énoncés et Corrigés]] +
  
-{{:cours:upload:2-7-2-2018-exo-tauto.pdf|Exercice}} à rendre avant le 8 novembre. 
 ==== Pré-requis ==== ==== Pré-requis ====
  
Line 99: Line 89:
  
 </dl></html> </dl></html>
 +
 ==== Cours liés ==== ==== Cours liés ====
  
-Ce cours s'appuie sur le cours de M2 //[[c-2-7-1|Fondements des systèmes de preuves]]//. Certaines notions du cours //[[c-2-5|démonstration automatique]]// peuvent être utiles.+Ce cours s'appuie sur le cours de M2 //[[c-2-7-1|2-7-1: Fondements des systèmes de preuves]]//. Certaines notions du cours //[[c-2-5|2-5: démonstration automatique]]// peuvent être utiles.
  
-En complément, le cours //[[c-2-36-1|Preuves de programmes]]// est particulièrement indiqué.+En complément, le cours //[[c-2-36-1|2-36-1: Preuves de programmes]]// est particulièrement indiqué.
  
 ==== Stages liés au cours ==== ==== Stages liés au cours ====
Line 125: Line 116:
  
  
-==== Les années précédentes ==== 
- 
-Annales: 
- 
-   * {{:cours:upload:2-7-2-examen1516.pdf|Examen 2015-2016}} 
-   * {{:cours:upload:2-7-2-exam1415.pdf|Examen 2014-2015}} 
-   * [[http://www.lix.polytechnique.fr/~barras/mpri|Sujets examens et projets]] 
  
 ==== Équipe pédagogique ==== ==== Équipe pédagogique ====
 
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