#acl +All:read

= Assistants de preuves =
== Infos ==
Enseignants : [[https://yforster.github.io/|Yannick Forster]] et [[https://theowinterhalter.github.io/|Théo Winterhalter]]

Salle : 1002 in Bâtiment Sophie Germain

Heure : Lundi de 8h45 à 11h45

== Évaluation ==
1/2 Projet + 1/2 Examen

Informations : 

 * Projet : En Coq 8.16.1 RESPECTER la version (pas besoin des modules sauf pour les questions bonus).
 Publié le 09/10/23, à rendre pour le 20/11/23 à 21h00. Lien [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_project.pdf|ICI]]. Consiste en trois exercices à rendre et un pdf ou expliquant ce qui est fait. Toutes les connaissances pour l'exercice 1 sont déjà données au cours 4. Celles pour le reste le sont au cours 5.

 * Examen : probablement le 27 Novembre de 08h45 à 11h45. Droit à une feuille A4 manuscrite recto verso.

== Contenu ==

=== Cours 1 ===
==== Cours ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri-coq-23-1.pdf|Slides]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2_7_2_2023_live_coding_1.v.txt|Code du cours]]
==== TD ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:tp1.v.txt|TD]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri-2-7-2-2023-tp1c.v.txt|Solutions]]

=== Cours 2 ===
==== Cours ====
 * Pas de slides.
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_live_coding_2.v.txt|Code du cours]]
==== TD ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_tp2.v.txt|TD]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri-2-7-2-2023-tp2c.v.txt|Solutions]]
==== Exercices avancés ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_advanced_ex_cantor.v.txt|Cantor pairing]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2_7_2_2023_2_cantor_sol.v.txt|Solutions Cantor pairing]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_advanced_ex_church.v.txt|Church numbers]]
 * [[https://gist.github.com/yforster/8c90a2174f684964259c6732fd90aaea|Solutions Church numbers]]

=== Cours 3 ===
==== Cours ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2023-3.pdf|Slides]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri-coq-23-3.pdf|Slides meta theory]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_live_coding_3.v.txt|Code du cours]]
==== TD ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_tp3.v.txt|TD]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_tp3c.v.txt|Solutions]]
==== Autres ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_reduction.v.txt|Règles de réductions]]
=== Cours 4 ===
==== Cours ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2_7_2_23_live_coding_4.v.txt|Code du cours]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2023_4_ex_definitional.pdf|Exercices]]
==== TD ====
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:mpri_2_7_2_2023_tp4.v.txt|TD]]


== Informations supplémentaires ==
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2-7-2-examen1718.pdf|Examen 17-18]] [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2-7-2-2018-exam-sol.v.txt|Solutions en Coq]]
 * [[https://wikimpri.dptinfo.ens-cachan.fr/lib/exe/fetch.php?media=cours:upload:2-7-2-examen1516.pdf|Examen 15-16]]