Abstract | ||
---|---|---|
This paper provides a sound foundation for autonomous objects communicating by remote method invo- cations and futures. As a distributed extension of @z-calculus, we define ASP"f"u"n, 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 ASP"f"u"n calculus and its semantics. Secondly we provide a type system for ASP"f"u"n, which guarantees the ''progress'' property. Most importantly, ASP"f"u"n 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. |
Year | DOI | Venue |
---|---|---|
2009 | 10.1016/j.entcs.2009.10.026 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
concise representation,good step,object language,theorem proving,autonomous object,functional object,distribution,n calculus,futures,asynchronous method invoca,object calculus,typing,request-reply mechanism,functional active objects,remote method invo,isabelle theorem prover,type system,distributed objects,theorem prover | Distributed object,Programming language,Object-based language,Computer science,Automated theorem proving,Theoretical computer science,Asynchronous method invocation,Semantics | Journal |
Volume | ISSN | Citations |
255, | Electronic Notes in Theoretical Computer Science | 4 |
PageRank | References | Authors |
0.45 | 18 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ludovic Henrio | 1 | 304 | 34.43 |
Florian Kammüller | 2 | 184 | 26.62 |