Enseignement de Sylvie Boldo
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.