A Formalization of the Theory of Objects in Isabelle/HOL

Ludovic Henrio 1 Florian Kammüller 2
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present a formalization of Abadi's and Cardelli's theory of objects in the interactive theorem prover Isabelle/HOL. In particular, we present (a) a formal model of objects and its operational semantics based on DeBruijn indices (b) a parallel reduction relation for objects (c) the proof of confluence for the theory of objects reusing Nipkow's HOL-framework for the lambda calculus.
Type de document :
Rapport
[Research Report] RR-6079, INRIA. 2006, pp.17
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00121816
Contributeur : Ludovic Henrio <>
Soumis le : mardi 6 février 2007 - 14:48:28
Dernière modification le : mardi 12 juin 2018 - 10:04:04
Document(s) archivé(s) le : mardi 21 septembre 2010 - 12:36:11

Fichiers

RR-Sigma.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00121816, version 2

Collections

Citation

Ludovic Henrio, Florian Kammüller. A Formalization of the Theory of Objects in Isabelle/HOL. [Research Report] RR-6079, INRIA. 2006, pp.17. 〈inria-00121816v2〉

Partager

Métriques

Consultations de la notice

325

Téléchargements de fichiers

161