Skip to Main content Skip to Navigation
Reports

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.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00186963
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, November 13, 2007 - 3:15:18 PM
Last modification on : Monday, December 28, 2020 - 10:22:04 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 3:15:47 PM

Files

RR-6353.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

340

Files downloads

366