LIP6 2004/002

• Rapports de recherche «BBFoc»
• S. Fechter, O. Boite
• 19 pages - 04/05/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
Cet article décrit un modèle d'un langage de programmation et de spécifications de structures algébriques pour le calcul formel. Ce modèle comporte un aspect orienté objet, et une notion nouvelle de type support pour les entités manipulées. L'article décrit la preuve mécanisée de la sûreté du typage du modèle avec le système coq.