Skip to main content

Higher-order action calculi

  • Conference paper
  • First Online:
Book cover Computer Science Logic (CSL 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 832))

Included in the following conference series:

Abstract

Action calculi are a broad class of algebraic structures, including a formulation of Petri nets as well as a formulation of the π-calculus. Each action calculus HAC(K) is generated by a particular set K of operators called controls. The purpose of this paper is to extend action calculi in a uniform manner to higher-order. A special case is essentially the extension of the π-calculus to higher order by Sangiorgi. To establish a link between the interactive and functional paradigms of computation, a variety of the λ-calculus is obtained as the extension of the smallest action calculus HAC(θ).

The dynamics of higher-order action calculi is presented, blending communication -for example in process calculi- with reduction as in the λ-calculus. Strong normalisation is obtained for reduction. A set of equational axioms is given for higher-order action calculi. Taking the quotient of HAC(θ) by a single extra axiom η, a cartesian-closed category is obtained.

An ultimate goal of the paper is to combine process calculi and functional calculi, both in their formulation and in their semantics.

This work was done with the support of a Senior Fellowship from the Science and Engineering Research Council, UK.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, ACMPOPL Conference, San Francisco, 1990.

    Google Scholar 

  2. Asperti, A. and Laneve, C., Interaction systems, Proc. International Workshop on Higher-order algebra, Logic and Term rewriting, Amsterdam, September 1993.

    Google Scholar 

  3. Asperti, A. and Longo, G., Categories, Types and Structures, MIT Press, 1991.

    Google Scholar 

  4. Barendregt, H., The Lambda Calculus, North Holland 1981.

    Google Scholar 

  5. Berry, G. and Boudol, G., The chemical abstract machine, Journal of Theoretical Computer Science, Vol 96, pp 217–248, 1992.

    MathSciNet  Google Scholar 

  6. Danos, V. and Regnier, L., Local and asynchronous beta-reduction, Proc. LICS, Montreal, 1993.

    Google Scholar 

  7. Giacalone, P., Mishra, P. and Prasad, S., Facile: a symmetric integration of concurrent and functional programming, International Journal of Parallel Programming, Vol 18, pp121–160, 1989.

    Article  Google Scholar 

  8. Gunter, C.A., Semantics of Programming Languages, MIT Press, 1992.

    Google Scholar 

  9. Lambek, J. and Scott, P.J., Introduction to Higher-order Categorical Logic, Cambridge University Press,1986.

    Google Scholar 

  10. Milner, R., The polyadic π-calculus: a tutorial, in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993.

    Google Scholar 

  11. Milner, R., Action structures and the π-calculus, to appear in Proceedings of NATO Advanced Study Institute on Proof and Computation (held at Marktoberdorf, 1993), about 60pages. (This paper combines of two previous reports: Action structures, Research Report ECS-LFCS-92-249, and Action structures for the π-calculus, Research Report ECS-LFCS-93-264, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University.

    Google Scholar 

  12. Milner, R., Action calculi I: axioms and applications, Computer Science Department, Edinburgh University, 1993. Also appeared as Action calculi, or syntactic action structures, Proceedings of MFCS '93, Lecture Notes in Computer Science Vol 711, Springer-Verlag, pp105–121, 1993.

    Google Scholar 

  13. Milner, R., Action calculi II: π-nets with boxes and replication, Computer Science Department, Edinburgh University, 1993.

    Google Scholar 

  14. Milner, R., Parrow, J. and Walker, D., A calculus of mobile processes, Parts I and II, Journal of Inf. and Comp, Vol 100, pp1–40 and pp41–77, 1992.

    MathSciNet  Google Scholar 

  15. Petri, C.A., Fundamentals of a theory of asynchronous information flow, Proc. IFIP Congress '62, North Holland, pp386–390, 1962.

    Google Scholar 

  16. Pierce, B.C., Programming in the π-calculus, Draft, Computer Science Department, University of Edinburgh, 1993.

    Google Scholar 

  17. Pitts, A.M. and Stark, I.D.B., Observable properties of higher-order functions that dynamically create local names, or: What's new?, Proc. MFCS'93, Lecture Notes in Computer Science Vol 711, Springer-Verlag, pp122–141, 1993.

    Google Scholar 

  18. Ritter, E., Normalization for Typed Lambda Calculi with Explicit Substitution, Paper presented at the 1993 Annual Conference of the European Association for Computer Science Logic, Swansea 1993.

    Google Scholar 

  19. Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-order paradigms, PhD Thesis, CST-99-93, Computer Science Department, University of Edinburgh, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Egon Börger Yuri Gurevich Karl Meinke

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Milner, R. (1994). Higher-order action calculi. In: Börger, E., Gurevich, Y., Meinke, K. (eds) Computer Science Logic. CSL 1993. Lecture Notes in Computer Science, vol 832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0049335

Download citation

  • DOI: https://doi.org/10.1007/BFb0049335

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58277-9

  • Online ISBN: 978-3-540-48599-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics