Assistants de preuves

Infos

Enseignants : Yannick Forster et 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 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

• Slides

• Code du cours

TD

• TD

• Solutions

Cours 2

Cours

• Pas de slides.

• Code du cours

TD

• TD

• Solutions

Exercices avancés

• Cantor pairing

• Solutions Cantor pairing

• Church numbers

• Solutions Church numbers

Cours 3

Cours

• Slides

• Slides meta theory

• Code du cours

TD

• TD

• Solutions

Autres

• Règles de réductions

Cours 4

Cours

• Code du cours

• Exercices

TD

• TD

Informations supplémentaires

• Examen 17-18 Solutions en Coq

• Examen 15-16