LIP6 2000/013

• Reports
  Spécification en Coq de la notion d'héritage utilisée en Calcul Formel
• S. Boulmé
• 15 pages - 05/31/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
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.
• Keywords : Ocaml, Coq, records, classes, objects, modules, dependent types, Curry-Howard, late binding, inheritance, library
• Publisher : David.Massot (at) nulllip6.fr