HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, November 13, 2007 - 3:15:18 PM
Last modification on : Friday, February 4, 2022 - 3:11:38 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 3:15:47 PM


Files produced by the author(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⟩



Record views


Files downloads