Next:
L'équipe
Proposition de projet Lemme :
Logiciels et Mathématiques
L'équipe
Introduction
Thèmes de recherche
Environnements de preuves
Moyens d'interaction
Maintenance des développements formels
Formalisation de théories mathématiques
Implémentations certifiées d'algorithmes de calcul scientifique
Positionnement vis-à-vis des autres projets issus de CROAP
Insertion dans la communauté scientifique
Collaborations effectives
A l'INRIA
Cornell, USA
Types
Calculemus
UITP (User-Interfaces for Theorem Provers)
Calcul formel
Collaborations à développer et contexte
A l'INRIA
Université Chalmers à Göteborg, Suède
Université d'Eindhoven, Hollande
Université de Cambridge, GB
Université de Nijmegen, Hollande
Université de Berkeley, USA
Mizar, Pologne
Université d'Edinbourg, Écosse
MathML
Risc Linz, Autriche
Relations industrielles
Certification de logiciel en Aéronautique
Dyade, France
Vérilog, France
Prover Technology, Suède
Utilisateurs de nos travaux.
Les utilisateurs du système Coq
Les industriels
Les étudiants et les enseignants
Applications potentielles
Télécommunications
Digilog, France
Cryptographie
Enseignement
Enseignement, formation, animation
DEA MDFI (Marseille/INRIA Sophia)
Maîtrise de mathématiques de l'UNSA (MASF, option informatique)
Stages
Thèses
Initiation à la preuve formelle
Organisation de conférence
Programme
Thème 1 : Environnements de preuve
Preuve par sélection et interprétation des mouvements
Connexion avec le Web
Reconnaissance de formules
Preuves textuelles
Thème 2 : Formalisation de théories mathématiques
Géométrie algébrique
Groupes et corps finis
Mathématiques du premier cycle universitaire
Géométrie
Thème 3 : Implémentations certifiées d'algorithmes
Preuves d'algorithmes
Extraction
Développement de compilateurs certifiés
Récursion bien fondée et simplification
Réflexion
Complexité
Objectifs à 3 ans
Références
Table des matières
Loic Pottier
1999-10-13
