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.
• Mots clés : langage orienté objet, héritage, semantique, typage, sûreté du typage, espèce, collections, type support
• Directeur de la publication : David.Massot (at) nulllip6.fr