A Mechanized Model of the Theory of Objects

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 : In this paper we present a formalization of Abadi's and Cardelli's theory of ob jects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL-framework for the analysis of a functional calculus for distributed ob jects. In particular, we present (a) a formal model of ob jects and its operational semantics based on de Bruijn indices (b) a parallel reduction relation for ob jects (c) the proof of confluence for the theory of ob jects reusing Nipkow's HOL-framework for the lambda calculus. We expect this framework to be highly reusable and allow further development and mechanized proofs of various aspects of ob ject theory, e.g., distribution, aspect orientation, typing.
Type de document :
Communication dans un congrès
9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), Jun 2007, CYPRUS, Springer, 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00150272
Contributeur : Ludovic Henrio <>
Soumis le : mardi 29 mai 2007 - 22:51:43
Dernière modification le : mardi 12 juin 2018 - 10:04:04
Document(s) archivé(s) le : jeudi 8 avril 2010 - 17:08:38

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00150272, version 1

Collections

Citation

Ludovic Henrio, Florian Kammüller. A Mechanized Model of the Theory of Objects. 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), Jun 2007, CYPRUS, Springer, 2007. 〈inria-00150272〉

Partager

Métriques

Consultations de la notice

253

Téléchargements de fichiers

319