Cours formel d'algèbre linéaire
Proposition de stage (niveau master 1)
Sujet:
Le logiciel Coq offre la possibilité
de formaliser les mathématiques. Le travail proposé consiste à
formaliser en Coq le cours d'algèbre de premième
année.
Encadrement:
Laboratoire d'accueil:
Prérequis:
Il est bien sûr souhaitable que le stagiaire ait déjà
eu un premier contact avec un logiciel de preuves et
qu'il ne soit pas rebuté par l'algèbre de première
année.
Matériel:
Table, chaise, papier, stylo-bille, tableau, craie, bibliothèque,
café, terminal, lumière(s).
Cette page est accessible par internet: http://math.unice.fr/~ah/stages/wims.html.