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.