Forschungsleitung (Direction de recherche) : Thérèse HARDIN

Conception et implantation du langage FoC pour le développement de logiciels certifiés

Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.

Publikationen 2001-2005

• 2005
  • D. Delahaye, M. Jaume, V. Prevosto : “Coq : un outil pour l’enseignement”, Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 24 (9), pp. 1139-1160, (Lavoisier) (2005)
• 2003
  • V. Prévosto : “Conception et implantation du langage FoC pour le développement de logiciels certifiés”, these, verteidigung einer doktorarbeit 15.09.2003, forschungsleitung (direction de recherche) Hardin, Thérèse (2003)
  • M. Maarek, V. Prevosto : “FoCDoC: The Documentation System of FoC”, Calculemus 2003 - 11^th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Roma, Italy, pp. 31-42 (2003)
  • V. Prevosto, M. Jaume : “Making proofs in a hierarchy of mathematical structures”, Calculemus 2003 - 11^th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, pp. 89-100, (Aracne) (2003)
• 2002
  • V. Prevosto, D. Doligez : “Algorithms and Proofs Inheritance in the FOC Language”, Journal of Automated Reasoning, vol. 29 (3-4), pp. 337-363, (Springer Verlag) (2002)
  • D. Doligez, Th. Hardin, V. Prevosto : “Algebraic Structures and Dependent Records”, TPHOLs'02 - 15^th International Conference on Theorem Proving in Higher-Order logics, vol. 2410, Lecture Notes in Computer Science, Hampton, VA, United States, pp. 298-313, (Springer) (2002)
  • V. Prevosto : “The FoC Project: Building a Certified Computer Algebra Library”, ISSAC 2002 - International Symposium on Symbolic and Algebraic Computation, Lille, France (2002)
  • D. Doligez, Th. Hardin, V. Prevosto : “FOC, a certified computer algebra library”, Automath'2002, Edinburgh, United Kingdom (2002)
• 2001
  • V. Prevosto : “Prototype d’interface utilisateur de la librairie Foc”, JFLA 2001 - 12^es Journées Francophones des Langages Applicatifs, Pontarlier, France (2001)