Exposés
Vizualising geometrical statements with Geoview (UITP 2003)
Proof of polynomial
inequalities in Coq
(Dagstuhl
seminar on «Verification and Constructive Algebra »
janv.2003,
and Summer
School on Computer Tools for Real Algebraic Geometry, Rennes,
juil. 2003)
Extraction de la sorte de Coq vers ocaml (JFLA2001)
Mathematics and proof presentation in pcoq (2001)
Extraction from Coq sort Type to ocaml (Types 2000)
Computation of Hilbert bases (ISMP, session on Hilbert bases, Lausanne 1997)
Programmes
utiliser Coq sur le Web.
Tester
(ça rame un peu: le serveur Web de Sophia tourne à
400Mhz...)
calcul de bases de Hilbert.
Tester,
télécharger le code
C.
preuves d'égalités
polynomiales en Coq: tactique Gb.
Résistances
Je l´avoue, j´utilise Windows XP, mais avec des logiciels libres... A propos, voila une pétition contre les brevets logiciels à signer vite.
Une autre pétition, pour soutenir l'emploi scientifique. Ça aussi c'est urgent.
La recherche publique est en danger, des infos sur ce site, par exemple.
Plus généralement, ces sites présentent
des infos moins pré-mâchées qu'ailleurs:
-
google actualités (du
Figaro à l'Humanité en passant par Politis).
-
marchandisation du
vivant
En vrac
en rentrant du boulot (en rêve)
à propos d'un problème d'avion posé par G.Dowek
mises à plat de polyèdres:
- quelques pages dans le livre
de Max Charvolen <<les portulans de l'immédiat>>(Editeur
Al Dante Eds
ISBN 2911073037). C'est de l'art moderne, j'ai pas tout compris,
mais pour la partie géométrique, ça va.
Et
puis c'est mon pote, je trouve ça joli ce qu'il fait.
-
un exemple de mise à plat,
- un
autre (mise à plat avec
recouvrement d'un polyèdre convexe).