Enseignement de Sylvie Boldo
En 2012, j'ai enseigné à l'école du GDR Informatique Mathématique à Rennes avec un polycopié de cours.
In 2011-2012, I taught for the MPRI in the 2-7-1 course "Foundations of proof systems" de Gilles Dowek. And here are the slides.
En 2009-2010, j'enseigne au MPRI dans le cours 2-7-1 "Fondements des systemes de preuves" de Gilles Dowek.
Voici les sujets des TPs et leur correction, très largement inspirés par ceux d'Alexandre Miquel et d'Assia Mahboubi:
- TP1 et sa correction en Coq 8.2 et sa correction en Coq 8.1.
- TP2 et sa correction en Coq 8.2 et sa correction en Coq 8.1.
- TP3 et sa correction en Coq 8.2 et sa correction en Coq 8.1.
- TP4 et sa correction en Coq 8.2 et sa correction en Coq 8.1.
- TP5 et sa correction (Coq 8.2 et Coq 8.1).
- TP6 et sa correction (Coq 8.2 et Coq 8.1).
- TP7 et sa correction en Coq 8.2 et sa correction en Coq 8.1.
- Cours sur les réels axiomatiques de Coq.