Skip to Main content Skip to Navigation
Reports

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
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00073382
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 12:40:18 PM
Last modification on : Friday, September 28, 2018 - 4:06:02 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:44:44 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

124

Files downloads

186