Sémantique Naturelle et Coq : vers la spécification et les preuves sur les langages à objets

Olivier Laurent 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Le système Centaur permet la description d'un langage de programmation en Sémantique Naturelle. Cette description peut être exécutée (en Prolog) et testée puis traduite en données pour le système Coq pour permettre la réalisationde preuves de propriétés de cette sémantique. Nous présentons ici les premiers pas dans l'application de cette approche aux langages à objets en s'appuyant sur le sigma-calcul défini par M.~Abadi et L.~Cardelli dans leur livre A Theory of Objects. La réalisation en Coq de la preuve de conservation des types (SRT) pour le sigma-calcul avec récursion et sous-typage (Ob1
Type de document :
Rapport
RR-3307, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073382
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:40:18
Dernière modification le : jeudi 11 janvier 2018 - 16:23:47
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:44:44

Fichiers

Identifiants

  • HAL Id : inria-00073382, version 1

Collections

Citation

Olivier Laurent. Sémantique Naturelle et Coq : vers la spécification et les preuves sur les langages à objets. RR-3307, INRIA. 1997. 〈inria-00073382〉

Partager

Métriques

Consultations de la notice

92

Téléchargements de fichiers

129