# zbMATH — the first resource for mathematics

Functional active objects: typing and formalisation. (English) Zbl 1364.68130
Salaün, Gwen (ed.) et al., Proceedings of the 8th international workshop on the foundations of coordination languages and software architectures (FOCLASA 2009), Rhodes, Greece, July 11, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 255, 83-101 (2009).
Summary: This paper provides a sound foundation for autonomous objects communicating by remote method invocations and futures. As a distributed extension of $$\varsigma$$-calculus, we define ASP$$_{\mathrm{fun}}$$, 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 invocations. This paper first presents the ASP$$_{\mathrm{fun}}$$ calculus and its semantics. Secondly we provide a type system for ASP$$_{\mathrm{fun}}$$, which guarantees the “progress” property. Most importantly, ASP$$_{\mathrm{fun}}$$ 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.
For the entire collection see [Zbl 1281.68038].

##### MSC:
 68N18 Functional programming and lambda calculus 68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
##### Keywords:
theorem proving; object calculus; futures; distribution; typing
Isabelle/HOL
Full Text: