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 <[email protected]>
To: Coq Club <[email protected]>
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
