Sujet:

La notion de catégorie de modèles, introduite dans les années soixante par Quillen, s'est imposée depuis comme la structure organisationnelle en théorie de l'homotopie. Le slogan est "là où il y a de l'homotopie, il doit y avoir une catégorie de modèles". Dans un récent travail [HM], Hirschowitz et Maggesi ont décrit une nouvelle catégorie de modèles concernant les "typoides", qui constitue un exemple assez élémentaire, mais non trivial. Enfin le logiciel Coq offre la possibilité de faire des preuves formelles sur ordinateur. Le travail proposé consiste à donner une preuve formelle, en Coq, du fait que les données indiquées dans [HM] constituent bien une catégorie de modèles. Bien entendu, le stagiaire bénéficiera, en début de stage, d'une formation gratuite au logiciel Coq.

Encadrement:

André Hirschowitz

Tel : 04 92 07 62 04

E-mail : ah@math.unice.fr

Laboratoire d'accueil:

Laboratoire J.A. Dieudonné

Equipe de géométrie projective
06108-Nice Cedex 2
FRANCE

Prérequis:

Le stagiaire devra avoir les connaissances de base concernant les catégories. D'ailleurs le candidat stagiaire allergique aux catégories peut négocier: les mathématiques intéressantes à formaliser ne manquent pas.

Retour à la liste des stages proposés.

Cette page est accessible par internet: http://math.unice.fr/~ah/stages/cmf.html.