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. https://doi.org/10.1016/j.entcs.2009.10.026