[FB02] BBFoc
Rapport Scientifique :
Date de dépot: 2002/01/01,
Nb pages 19,
(Tech. Rep.: CEDRIC-02-685)
motcle:
Résumé:
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.