ASPfun: A Functional and Distributed Object Calculus Semantics, Type-system, and Formalization

Ludovic Henrio 1 Florian Kammüller 2 Henry Sudhof 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 : Several paradigms exist for distributed computing, this paper tries to provide a sound foundation for autonomous objects communicating in a very structured way. We define ASPfun, a calculus of functional objects, behaving autonomously, and communicating by a request-reply mechanism: requests are method calls handled asynchronously, futures represent awaited results for requests, and replies return the result of a request to an object that holds the corresponding future. This report first presents the ASPfun calculus and its semantics. Secondly we provide a type system for ASPfun, which ensure the ``progress'' property: while there is a request that is not reduced to a value, the computation can continue. ASPfun and its properties have been formalized and proved using the Isabelle theorem prover.
Type de document :
[Research Report] RR-6353, INRIA. 2007, pp.18
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 13 novembre 2007 - 15:15:18
Dernière modification le : mardi 12 juin 2018 - 10:04:04
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:15:47


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00186963, version 2



Ludovic Henrio, Florian Kammüller, Henry Sudhof. ASPfun: A Functional and Distributed Object Calculus Semantics, Type-system, and Formalization. [Research Report] RR-6353, INRIA. 2007, pp.18. 〈inria-00186963v2〉



Consultations de la notice


Téléchargements de fichiers