ASPfun: a typed functional active object calculus
Article
Henrio, L., Kammueller, F. and Lutz, B. 2012. ASPfun: a typed functional active object calculus. Science of Computer Programming. 77 (7-8), pp. 823-847. https://doi.org/10.1016/j.scico.2010.12.008
Type | Article |
---|---|
Title | ASPfun: a typed functional active object calculus |
Authors | Henrio, L., Kammueller, F. and Lutz, B. |
Abstract | This paper provides a sound foundation for autonomous objects communicating by remote method invocations 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 an object language enabling a concise representation of a set of active objects interacting by asynchronous method invocations. This paper first presents the ASPfun calculus and its semantics. Then, we provide a type system for ASPfun which guarantees the “progress” property. Most importantly, ASPfun has been formalised; its properties have been formalised and proved using the Isabelle theorem prover and we consider this as an important step in the formalization of distributed languages. This work was also an opportunity to study different binder representations and experiment with two of them in the Isabelle/HOL theorem prover. |
Keywords | Theorem proving; object calculus; futures; distribution; typing; binders |
Research Group | Artificial Intelligence group |
Foundations of Computing group | |
Publisher | Elsevier |
Journal | Science of Computer Programming |
ISSN | 0167-6423 |
Publication dates | |
01 Jul 2012 | |
Online | 12 Jan 2011 |
Publication process dates | |
Deposited | 25 May 2012 |
Accepted | 28 Dec 2010 |
Output status | Published |
Copyright Statement | preprint as permitted by publisher. |
Digital Object Identifier (DOI) | https://doi.org/10.1016/j.scico.2010.12.008 |
Language | English |
First submitted version |
https://repository.mdx.ac.uk/item/83q45
Download files
73
total views9
total downloads3
views this month0
downloads this month