[isabelle-dev] Cours video d'introduction à Coq (fwd)

[Makarius]

Since videos for theorem provers were just mentioned, maybe this gives 
some inspiration, although it is much more educational than was probably 
intended for Isabelle/jEdit.

It is also possible to learn some French there ...


 	Makarius

---------- Forwarded message ----------
Date: Sat, 19 Jan 2013 08:32:07 -0500
From: bertot <Yves.Bertot at inria.fr>
To: Coq Club <coq-club at inria.fr>
Subject: [Coq-Club] Cours video d'introduction à Coq

(The link advertised in this message points to a collection of video lessons to 
teach Coq at introductory level, the courses are in French, so I will switch to 
French in the rest of this message).

Bonjour,

Vous trouverez sur la page http://fuscia.info/cours/coq/ un cours vidéo 
d'introduction à Coq, entièrement en Français, avec des leçons en deux formats 
différents.  D'une part des conférences avec transparents, d'une durée 
n'excédant pas 15 minutes et pour total de 8 heures.  D'autre part des 
démonstrations d'utilisation de Coq, avec commentaire en voix off.

Je tiens à remercier le partenariat Fuscia et l'UNT UNIT, en particulier 
Patrick Rambert pour l'aide apportée dans la préparation de ce cours.

Ce cours complète d'autres matériels en langue française auxquels j'ai 
participé:

1/ un cours d'introduction à Coq au niveau de première année de Master.

http://www-sop.inria.fr/members/Yves.Bertot/coq-master1.html

Pour les enseignants qui incorporent des étudiants étrangers dans leur 
audience, il peut être intéressant de noter que l'ensemble des cours 
disponibles sur cette page est également disponible en anglais.  Il est donc 
possible de faire un cours en français reposant sur cette introduction et de 
fournir les notes de cours en anglais pour les étudiants étrangers.  Notez que 
ces notes de cours fournissent une collection d'exercices.

2/ Pour une étude plus approfondie de Coq, je conseille de se tourner ver le 
livre écrit par Pierre Castéran et moi-même le Coq'Art ( 
http://www.labri.fr/Perso/%7Ecasteran/CoqArt/index.html ) en particulier, la 
version française du livre est disponible intégralement sur ce site ou en 
suivant le lien suivant: 
http://www.inria.fr/sophia/members/Yves.Bertot/coqartF.pdf

Le site du Coq'Art fournit également la collection de tous les exercices du 
livre et leur correction.

La page http://coq.inria.fr/cocorico/Other%20Coq%20Resources donne également 
accès à d'autres ressources en langue française pour l'enseignement de Coq.

Yves Bertot