Cours d'introduction à Coq

Cours d'introduction à la logique et à Coq

Supports de cours
Exercice corrigé

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

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

TP 2 : Logique de Hoare et preuves de programmes

Sujet de TP
Squelette associé au TP