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-1 [2018/11/21 09:07]
dowek [Past exams]
cours:c-2-7-1 [2019/11/12 06:18] (current)
werner [Exam]
Line 10: Line 10:
 ==== Teaching in 2018-2019 ==== ==== Teaching in 2018-2019 ====
  
-[[http://http://www.lsv.fr/~dowek/|Gilles Dowek]]+[[http://www.lix.polytechnique.fr/~werner/|Benjamin Werner]] 
 +and [[http://www.strub.nu/|Pierre-Yves Strub]]
  
 +==== Course Page ====
  
 +[[http://www.enseignement.polytechnique.fr/informatique/MPRI/2-7-1/|Here]]
  
 ==== Objectives ==== ==== Objectives ====
Line 20: Line 23:
 proof systems such as Coq, Agda, HOL, Isabelle, PVS. In particular we will treat in depth the articulation between reasoning and computation.  proof systems such as Coq, Agda, HOL, Isabelle, PVS. In particular we will treat in depth the articulation between reasoning and computation. 
  
-This course is a prerequisite to the course //Assistants de preuve : principes et application à la preuve de programmes//. 
  
 ==== When and where ? ==== ==== When and where ? ====
  
-The lectures are each Wednesday from 8:45 to 12:00, in the Sophie Germain Building, room 1004+The lectures are each Tuesday from 8:45 to 12:00, in the Sophie Germain Building, room 1013
  
  
Line 30: Line 32:
  
 <html><dl> <html><dl>
-<dt> September 12th: Natural deduction - The notion of theory+<dt> September 10thInductive definitions. Natural deduction
  
-<dt> September 19thThe notion of model Exercises+<dt> September 17thLogical and axiomatic cuts Arithmetic
  
-<dt> September 26th:  Arithmetic Naive set theory+<dt> September 24th:  Normalization of simply typed lambda-calculus and System T
  
-<dt> October 3rdSimple type theory Exercises+<dt> October 1stHigher-Order Logic
  
-<dt> October 10th: The termination of proof reduction +<dt> ...
- +
-<dt> October 17th:  Dependent types - Exercises +
- +
-<dt> October 31st: Inductive types - Polymorphism +
- +
-<dt> November 14th: Master class - Preparation of the exam+
 </dl> </dl>
 </html> </html>
  
-No lectures on October 24th and November 7th 
  
 ==== Exam ==== ==== Exam ====
  
-November 21st, 9h-10h30, Sophie Germain Buildingroom 1003+Tuesday, Nov. 19th 2019, 9h-11h301013. Course notes and personal documents allowed
  
 ==== Prerequisites ==== ==== Prerequisites ====
Line 68: Line 63:
 </html> </html>
  
-==== Bibliography ==== 
  
-<html> +==== Internships (last year - to be updated) ====
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit.pdf">Lecture notes</a> +
-<br> +
-Slides: <a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit1.pdf">Lecture 1</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit2.pdf">Lecture 2</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit3.pdf">Lecture 3</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit4.pdf">Lecture 4</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit5.pdf">Lecture 5</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit6.pdf">Lecture 6</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit8.pdf">Lecture 7</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit9.pdf">Lecture 8</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit10.pdf">Lecture 9</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit11.pdf">Lecture 10</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/pit12.pdf">Lecture 11</a>. +
- +
-<br> +
-Exercises: <a href = "http://www.lsv.fr/~dowek/Cours/Pit/exercises1.pdf">Exercises 1</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/exercises2.pdf">Exercises 2</a>, +
-<a href = "http://www.lsv.fr/~dowek/Cours/Pit/exercises3.pdf">Exercises 3</a>. +
-</html> +
-==== Internships ====+
  
 <html> <html>
 
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