LIP6 2004/002

• Reports
  BBFoc
• S. Fechter, O. Boite
• 19 pages - 05/04/2004- document en - http://www.lip6.fr/lip6/reports/2004/lip6.2004.002.pdf - 265 Ko
• Contact : stephane.fechter (at) nulllip6.fr
• Ancien Thème : SPI
This article describes a model for a programmation and algebraic structure specification language for the computer algebra. This model have an object oriented aspect, and a new notion of carrier type for handled entities. This article describe the mechanised proof of the type soundness of the model with the Coq system.
<Towards_a_formal_def.ps><bbfoc.ps>
• Keywords : oriented object language, inheritance, semantics, typing, type soundness, species, collections, carrier type
• Publisher : David.Massot (at) nulllip6.fr