OOIS’94 pp 37-53 | Cite as

Formalising Actors in Linear Logic

  • John Darlington
  • Yi-ke Guo


We present a logical formalism of the actor-based concurrent object oriented computation in terms of the deduction in linear logic. By encoding messages and objects in the actor model as formulae of linear logic, the distributed state of the actor computation, regarded as a configuration, can be represented as a multiset of object formulae and message formulae. Methods are encoded as a special form of logical implication describing the effect of the communication between objects and messages. With this logical encoding, actor based concurrent computation can be fully modelled as a deduction procedure in linear logic. In the paper, we provide a detailed mapping of the actor model into the logical system. It is shown that, with such a mapping, the logical semantics of actors can be developed.


Actor Model Linear Logic Mail Address Sequent Calculus Asynchronous Communication 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Abr90]
    Samson Abramsky. Computational Interpretation of Linear Logic. Technical report, Dept. of Computing, Imperial College, Oct. 1990.Google Scholar
  2. [AH88]
    Gul Agha and Carl Hewitt. Concurrent Programming Using Actors. In A. Yonezawa and M. Tokoro, editors, Object-Orientde Concurrent Programming, pages 37–54. The MIT Press, 1988.Google Scholar
  3. [BG90]
    Gerard Boudol and G. Berry. The chemical abstract machine. In Proc. of the 17th Annual ACM symposium on Principle of Programming Languages. ACM, 1990.Google Scholar
  4. [DG92]
    J. Darlington and Y. Guo. Definitional constraint programming for parallel computing: An introduction. In Proc. of the ICOT workshop on Future Direction of Parallel Programming and Architecture, June 1992. ICOT TM-1185.Google Scholar
  5. [DG94]
    John Darlington and Yike Guo. Towards a logical theory of object-based concurrency. Technical report, Imperial College, May 1994.Google Scholar
  6. [Gir87]
    Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1), 1987.Google Scholar
  7. [Guo93]
    Yike Guo. Definitional Constraint Programming. PhD thesis, Dept. of Computing, Imperial College, December 1993.Google Scholar
  8. [HT91]
    K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In Proc. of ECOOP’91 Workshop, LNCS 612, pages 21–51, 1991.Google Scholar
  9. [KY94]
    Naoki Kobayashi and Akinori Yonezawa. Type-theoretic foundations for concurrent object. Technical report, Dept of Information Science, 1994.Google Scholar
  10. [Mes89]
    Jose Meseguer. General logics. Technical Report SRI-CSL-89–5, SRI International, March 1989.Google Scholar
  11. [MW91]
    Jose Meseguer and Timothy Winkler. Parallel programming in maude. Technical Report SRI-CSL-91–08, SRI International, November 1991.Google Scholar

Copyright information

© Springer-Verlag London Limited 1995

Authors and Affiliations

  • John Darlington
    • 1
  • Yi-ke Guo
    • 1
  1. 1.Department of ComputingImperial CollegeLondonUK

Personalised recommendations