Ce travail s'inscrit dans un projet ambitieux (projet FOC du LIP6) qui 
consiste à essayer de programmer une bibliothèque de Calcul Formel qui soit 
certifiée. Cela signifie que les unités de la bibliothèque vont non seulement 
contenir des programmes, mais aussi des spécifications (ou des propriétés) 
vérifiées par ces programmes, et enfin des preuves que les programmes 
vérifient les spécifications. Ces preuves seront elles-mêmes vérifiées 
automatiquement par un assistant à la démonstration (Coq en l'occurrence...)

De plus, conformément aux langages modernes de développements de bibliothèques 
de Calcul Formel tels que Axiom ou Aldor, on souhaite que l'utilisateur puisse 
enrichir ou modifier facilement les unités afin de pouvoir suivre les 
améliorations algorithmiques sans cesse apportées par la recherche dans ce 
domaine.

Ces deux aspects ont conduit à choisir Ocaml, comme langage de programmation, 
car c'est un langage avec des modules et des objets pour exprimer la 
modularité, et dont la sémantique a été fortement étudiée. Ce langage produit 
de plus des programmes efficaces...

Pour programmer ces bibliothèques, il a fallu dégager un "style" mélangeant 
objets et modules adapté au Calcul Formel. Vu la nature "algébrique" des 
unités de bibliothèque du Calcul Formel, il s'agissait d'être proche d'une 
description "types abstraits de données". Ce style devait profiter des traits 
de la programmation objet (méthodes virtuelles ou par défaut, héritage, 
liaison tardive) et des modules (abstraction de type, foncteurs) qui 
permettent une grande réutilisation de code.

On montrera aussi pendant l'exposé, un dÝbut de formalisation de ce "style" en 
Coq, qui devrait permettre à terme d'exprimer spécifications et preuves de (et 
dans) ces unités de bibliothèques.

Page maintenue par Emmanuel Chailloux, dernière modification le 08/12/99 à 18h08

---

PPS

UFR P6