Projet Logique

Cette UE optionnelle de 6 ECTS se découpe en 14 séances de 1h30

Horaires

• Les séances de TP ont lieu le lundi de 10h30 à 12h.
• Le tutorat (optionnel) a lieu le mardi de 12h45 à 13h45.

(voir emploi du temps L3).

Modalité d'évaluation : Votre note finale sera la moyenne des 2 projets.

Matériel pour les séances de TPs

• Première partie : Agda (4 séances)

Cette partie est tirée du cours INF551 – Computational logic: from Artificial intelligence to Zero bugs de Samuel Mimram.

Ressources : Pattern matching avec with https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html

• TP 1 : Propositional logic in Agda, correction.
• TP 2 : Inductive types, correction.

• Projet Agda, à rendre pour le 4 mars, 10h30. Correction.
• Seconde partie : Coq (10 séances)
  • TP1 : Prouver en Coq, Correction.
  • TP2 : Types inductifs, Correction.
  • TP3 : Programmer en Coq, Correction.
  • TP4 : Extraction, Correction.
  • TP5 : Plus d'induction, Correction.
  • TP6 : Automatisation et tactiques, Correction.

Ressources :

• Résumé des tactiques et de la syntaxe
• version plus avancée.

• Projet de Coq : Grammaires.

À rendre pour le 2 juin.

Contact

Pour toutes questions, vous pouvez me contacter contacter à l'adresse : vialard (at) lmf (dot) cnrs (dot) fr