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 , Laboratoire I3S - 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 :
Rapport
[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

https://hal.inria.fr/inria-00186963
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 13 novembre 2007 - 15:15:18
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:15:47

Fichiers

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

Identifiants

  • HAL Id : inria-00186963, version 2

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

292

Téléchargements de fichiers

224