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>