Action Concertée Incitative

Nouvelles Interfaces des Mathématiques

Projet Mao -- Mathématiques assistées par ordinateur

Description courte du projet

Le premier volet de notre activité à venir concerne le logiciel Coq pour lequel nous projetons des améliorations sur au moins quatre points:

• le polymorphisme d'univers
• le système de modules
• le langage de tactiques
• la gestion des ressources méta-logiques.

Ces caractéristiques existent déjà dans Coq, mais sous des formes beaucoup trop rudimentaires.

Le second volet de notre activité concerne l'interface. Le projet Lemme, qui a déjà une solide expérience en la matière, a repris récemment notre problème d'interface à zéro, pour mieux satisfaire nos exigences, et les débuts de cette nouvelle entreprise sont déjà très prometteurs.

C'est le troisième volet de notre activité. Nous projetons d'implémenter en priorité la géométrie algébrique, et atteindre dès que possible le niveau recherche. Comme nous l'avons dit plus haut, il n'est pas nécessaire pour ça d'attendre de disposer d'une bibliothèque complète. Dans certains cas limités, on peut déjà utiliser Coq, comme le font nos cobayes. Nous comptons recruter et former régulièrement de nouveaux cobayes et orienter de plus en plus la programmation de la bibliothèque en fonction de leurs besoins.

Chemin faisant, nous avons rencontré et rencontrerons encore des questions théoriques concernant cette affaire et nous nous faisons un devoir de les traiter.

Ainsi la place privilégiée tenue par la structure de monade nous a conduits à formuler une caractérisation du lambda-calcul pur comme monade "exponentielle" initiale, un théorème dont la première démonstration (en bonne voie) sera formelle.

Parmi les questions méta-théoriques pendantes, on peut déjà citer

• le problème du polymorphisme d'univers,
• le problème abstrait de la dissociation calculs/preuves,
• le problème du "late-proving": on veut une variante du calcul des constructions permettant de différer les obligations de preuve pendant la construction d'un terme (ce problème est liée à l'intégration du principe de proof-irrelevance, ainsi qu'au problème précédent).

Nous allons très bientôt mettre en place un site permettant d'utiliser notre interface de mathématiques interactives et notre bibliothèque, qui permettra à l'utilisateur de commencer à travailler à partir d'un simple navigateur. Bien entendu, nos produits y seront documentés.

(dernière mise à jour du site : 14 décembre 2004)

Coordinateur du projet

Partenaires

Objectifs

Projets

Démos

Contexte

Présentations

Activités