Cours d'introduction à Coq

Cours d'introduction à la logique et à Coq

Supports de cours

TP 1 : Preuves de compilation et d'optimisation d'expressions

Sujet de TP (expressions, optimisation, compilation vers un langage à pile)
Squelette associé au TP

Cours 2

Cours 2 : qu'est ce qu'on peut faire avec Coq et les méthodes formelles ?

TP 2 : Logique de Hoare et preuves de programmes

Sujet de TP
Squelette associé au TP