Evènement pour le groupe Combinatoire Énumérative et Algébrique


Date 2018-12-24  10:45-11:45
TitreCombinatoire algébrique en Coq/MathComp 
RésuméDans cet exposé, je présenterai mon travail de formalisation sous le système Coq/MathComp d'un certain nombre de résultats de combinatoire algébrique, notamment la règle de Littlewood Richardson, les caractères des groupes symétriques et la formule des équerres. Cet exposé se veut introductif et ne suppose pas de familiarité avec les systèmes de preuves formelles. Après une introduction au système Coq/MathComp, j'essayerai de donner une idée de la démarche, de l'intérêt et des difficultés d'un tel travail de formalisation. Le résultat du travail est accessible sur https://github.com/hivert/Coq-Combi. Il a bénéficié de contributions de Thibaut Benjamin, Jean Christophe Filliâtre, Christine Paulin et Olivier Stietel.  
Lieu076 
OrateurFlorent Hivert 
EmailFlorent.Hivert@lri.fr 
UrlUniversité Paris-Sud, LRI 



Aucun document lié à cet événement.

Retour
Retour à l'index