Functional Active Objects: Typing and Formalisation

Citations of this article
Mendeley users who have this article in their library.


This paper provides a sound foundation for autonomous objects communicating by remote method invo- cations and futures. As a distributed extension of ζ-calculus, we define ASPfun, a calculus of functional objects, behaving autonomously and communicating by a request-reply mechanism: requests are method calls handled asynchronously and futures represent awaited results for requests. This results in a well structured distributed object language enabling a concise representation of asynchronous method invoca- tions. This paper first presents the ASPfun calculus and its semantics. Secondly we provide a type system for ASPfun, which guarantees the "progress" property. Most importantly, ASPfun and its properties have been formalised and proved using the Isabelle theorem prover, and we consider it as a good step toward formalisation of distributed languages. © 2009 Elsevier B.V. All rights reserved.




Henrio, L., & Kammüller, F. (2009). Functional Active Objects: Typing and Formalisation. Electronic Notes in Theoretical Computer Science, 255, 83–101.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free