×

zbMATH — the first resource for mathematics

ASP\(_{\text{fun}}\) : a typed functional active object calculus. (English) Zbl 1242.68053
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\(_{\text{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 an object language enabling a concise representation of a set of active objects interacting by asynchronous method invocations. This paper first presents the ASP\(_{\text{fun}}\) calculus and its semantics. Then, we provide a type system for ASP\(_{\text{fun}}\) which guarantees the “progress” property. Most importantly, ASP\(_{\text{fun}}\) 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.
MSC:
68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Cardelli, L.: A theory of objects, (1996) · Zbl 0876.68014
[2] Pierce, B. C.: Types and programming languages, (2002) · Zbl 0995.68018
[3] Agha, G.: Actors: A model of concurrent computation in distributed systems, (1986)
[4] Agha, G.; Mason, I. A.; Smith, S. F.; Talcott, C. L.: A foundation for actor computation, Journal of functional programming 7, 1-72 (1997) · Zbl 0870.68091
[5] Hewitt, C.; Bishop, P.; Steiger, R.: A universal modular actor formalism for artificial intelligence, , 235-245 (1973)
[6] Agha, G.: An overview of actor languages, ACM SIGPLAN notices 21, 58-67 (1986)
[7] Caromel, D.; Delbé, C.; Di Costanzo, A.; Leyton, M.: Proactive: an integrated platform for programming and running applications on grids and P2P systems, Computational methods in science and technology 12, 69-77 (2006)
[8] Caromel, D.; Henrio, L.; Serpette, B.: Asynchronous and deterministic objects, , 123-134 (2004) · Zbl 1325.68052
[9] Caromel, D.; Henrio, L.: A theory of distributed objects, (2005) · Zbl 1084.68012
[10] Gordon, A. D.; Hankin, P. D.; Lassen, S. R. B.: Compilation and equivalence of imperative objects, Lncs (1997) · Zbl 0942.68025
[11] Johnsen, E. B.; Owe, O.; Yu, I. C.: Creol: a type-safe object-oriented model for distributed concurrent systems, Theoretical computer science 365, 23-66 (2006) · Zbl 1118.68031
[12] Nipkow, T.; Paulson, L. C.; Wenzel, M.: Isabelle/HOL–A proof assistant for higher-order logic, Lncs 2283 (2002) · Zbl 0994.68131
[13] Niehren, J.; Schwinghammer, J.; Smolka, G.: A concurrent lambda calculus with futures, Theoretical computer science 364, 338-356 (2006) · Zbl 1110.68023
[14] Henrio, L.; Kammüller, F.: A mechanized model of the theory of objects, Lncs (2007) · Zbl 1202.68097
[15] Aydemir, B.; Charguéraud, A.; Pierce, B. C.; Pollack, R.; Weirich, S.: Engineering formal metatheory, , 3-15 (2008) · Zbl 1295.68052
[16] B.E. Aydemir, A. Bohannon, N. Foster, B. Pierce, J. Vaughan, D. Vytiniotis, G. Washburn, S. Weirich, S. Zdancewic, M. Fairbairn, P. Sewell, The poplmark challenge, Web-site, 2008. · Zbl 1152.68516
[17] Bruijn, N. G. D.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes mathematicae 34, 381-392 (1972) · Zbl 0253.68007
[18] C. Urban, et al. Nominal methods group, Project funded by the German Research Foundation (DFG) within the Emmy-Noether Programme, 2006.
[19] Pitts, A. M.: Nominal logic, a first order theory of names and binding, Information and computation 186, 165-193 (2003) · Zbl 1056.03014
[20] Roeckl, C.; Hirschkoff, D.: A fully adequate shallow embedding of the \({\pi}\)-calculus in isabelle/hol with mechanized syntax analysis, Journal of functional programming 13, 415-451 (2003) · Zbl 1096.68679
[21] Ciaffaglione, A.; Liquori, L.; Miculan, M.: Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, JAR, journal of automated reasoning 39, 1-47 (2007) · Zbl 1118.68046
[22] Honsell, F.; Miculan, M.; Scagnetto, I.: Pi-calculus in (co)inductive-type theory, Theoretical computer science 253, 239-285 (2001) · Zbl 0956.68095
[23] Schmitt, A.: Safe dynamic binding in the join calculus, IFIP 96, 563-575 (2002)
[24] Ricci, A.; Viroli, M.; Piancastelli, G.: Simpa: an agent-oriented approach for programming concurrent applications on top of Java, Science of computer programming 76, 37-62 (2011) · Zbl 1211.68055
[25] Cardelli, L.: A language with distributed scope, , 286-297 (1995)
[26] Briais, S.; Nestmann, U.: Mobile objects ”must” move safely, IFIP conference Proceedings 209, 129-146 (2002) · Zbl 1048.68026
[27] A. Jeffrey, A distributed object calculus, in: ACM SIGPLAN Workshop Foundations of Object Oriented Languages.
[28] Gordon, A. D.; Hankin, P. D.; Lassen, S. B.: Compilation and equivalence of imperative objects, Lncs (1997) · Zbl 0942.68025
[29] Jr., R. H. Halstead: Multilisp: a language for concurrent symbolic computation, ACM transactions on programming languages and systems (TOPLAS) 7, 501-538 (1985) · Zbl 0581.68037
[30] Yonezawa, A.; Shibayama, E.; Takada, T.; Honda, Y.: Modelling and programming in an object-oriented concurrent language ABCL/1, Object-oriented concurrent programming, 55-89 (1987)
[31] Niehren, J.; Sabel, D.; Schmidt-Schauß, M.; Schwinghammer, J.: Observational semantics for a concurrent lambda calculus with reference cells and futures, Electron. notes theor. Comput. sci. 173, No. April, 313-337 (2007) · Zbl 1316.68034
[32] De Boer, F. S.; Clarke, D.; Johnsen, E. B.: A complete guide to the future, Lecture notes in computer science 4421, 316-330 (2007)
[33] Abrahám, E.; Grabe, I.; Grüner, A.; Steffen, M.: Behavioral interface description of an object-oriented language with futures and promises, Journal of logic and algebraic programming 78, 491-518 (2009) · Zbl 1187.68130
[34] Dedecker, J.; Cutsem, T. V.; Mostinckx, S.; D’hondt, T.; Meuter, W. D.: Ambient-oriented programming in ambienttalk, Lncs 4067, 230-254 (2006)
[35] A. Cansado, L. Henrio, E. Madelaine, Transparent first-class futures and distributed component, in: International Workshop on Formal Aspects of Component Software, FACS’08, in: Electronic Notes in Theoretical Computer Science (ENTCS), Malaga, 2008.
[36] J. Bengtson, J. Parrow, Formalising the pi-calculus using nominal logic, in: Proc. of the 10th International Conference on Foundations of Software Science and Computation Structures, FOSSACS, in: LNCS vol. 4423, 2007, pp. 63–77. · Zbl 1168.68436
[37] Bengtson, J.; Johansson, M.; Parrow, J.; Victor, B.: Psi-calculi: mobile processes, nominal data, and logic, , 39-48 (2009) · Zbl 1213.68399
[38] Ridge, T.: Operational reasoning for concurrent caml programs and weak memory models, Lncs 4732 (2007) · Zbl 1144.68305
[39] Flanagan, C.; Felleisen, M.: The semantics of future and an application, Journal of functional programming 9, 1-31 (1999) · Zbl 0926.68075
[40] Henrio, L.; Kammüller, F.: Functional active objects: typing and formalisation, Entcs 255, 83-101 (2009) · Zbl 1364.68130
[41] Fleck, A.; Kammüller, F.: Implementing privacy with Erlang active objects, (2010)
[42] F. Kammüller, Using functional active objects to enforce privacy, in: 5th Conf. on Network Architectures and Information Systems Security, SAR-SSI, 2010.
[43] Cole, M.: Bringing skeletons out of the closet: a pragmatic manifesto for skeletal parallel programming, Parallel computing 30, 389-406 (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.