Specifying in Coq inheritance used in Computer Algebra

S. Boulmé

LIP6 2000/013: Rapport de Recherche LIP6 / LIP6 research reports
15 pages - Mai/May 2000 - Document en anglais.

Get it : 94 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Sémantique, Preuve et Implantation

Titre français : Spécification en Coq de la notion d'héritage utilisée en Calcul Formel
Titre anglais : Specifying in Coq inheritance used in Computer Algebra

Résumé : Cet article s'inscrit dans le cadre de FOC, un projet de développement de bibliothèques de Calcul Formel certifiées en Coq. FOC a mis au point une méthodologie de programmation des bibliothèques de Calcul Formel, basée sur les objets et les modules de Ocaml. Afin de spécifier ces traits de modularité, nous donnons ici l'implémentation en Coq d'une théorie des enregistrements avec types dépendants. Cette théorie a en particulier pour but d'exprimer la notion d'héritage avec redéfinition de méthode et liaison tardive, utilisée dans les programmes FOC.

Abstract : This paper is part of FOC a project for developing Computer Algebra libraries, certified in Coq. FOC has developed a methodology for programming Computer Algebra libraries, using modules and objects in Ocaml. In order to specify modularity features used by FOC in Ocaml, we are coding in Coq a theory for extensible records with dependent fields. This theory intends to express especially the kind of inheritance with method redefinition and late binding, that FOC uses in its Ocaml programs.

Mots-clés : Ocaml, Coq, enregistrements, classes, objets, modules, types dépendants, Curry-Howard, liaison tardive, héritage, bibliothèque

Key-words : Ocaml, Coq, records, classes, objects, modules, dependent types, Curry-Howard, late binding, inheritance, library

Publications internes LIP6 2000 / LIP6 research reports 2000

Responsable Éditorial / Editor :David.Massot@lip6.fr