LIP6 2000/013

• Rapports de recherche
  Spécification en Coq de la notion d'héritage utilisée en Calcul Formel
• S. Boulmé
• 15 pages - 31/05/2000- document en - http://www.lip6.fr/lip6/reports/2000/lip6.2000.013.ps.gz - 96 Ko
• Contact : Sylvain.Boulme (at) nulllip6.fr
• Ancien Thème : SPI
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.
• Mots clés : Ocaml, Coq, enregistrements, classes, objets, modules, types dépendants, Curry-Howard, liaison tardive, héritage, bibliothèque
• Directeur de la publication : David.Massot (at) nulllip6.fr