Skip to main content
SpringerLink
Log in
Book cover

International Conference on Parallel Architectures and Languages Europe

PARLE 1989: PARLE '89 Parallel Architectures and Languages Europe pp 357–373Cite as

The typed λ-calculus with first-class processes

  • Submitted Presentations
  • Conference paper
  • First Online:

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

Abstract

We extend the typed λ-calculus with CCS- or CSP-like processes and allow these to be first-class citizens just as functions are first-class citizens in functional languages. The main novel feature of the language is the use of types to record the communication possibilities possessed by processes and in this we give up the causality between communications, i.e. the types do not model whether or not one communication may take place before another. In analogy with the semantics of the λ-calculus, and of CCS, we develop a structural operational semantics for the language. We then prove that the operational semantics preserves the types and we use this to give examples of ‘errors’ that cannot arise for well-typed programs.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.America, J.deBakker, J.N.Kok, J.Rutten: Operational Semantics of a Paralled Object-Oriented Language, Proceedings of the 1986 ACM Conference on Principles of Programming Languages, 1986, pp. 194–208.

    Google Scholar 

  2. E. Astesiano, E. Zucca: Parametric channels via label expressions in CCS, TCS 33 (1984) pp. 45–63.

    Google Scholar 

  3. H.P.Barendregt: The Lambda Calculus — Its Syntax and Semantics, North-Holland, 1984.

    Google Scholar 

  4. L.Cardelli: Amber, Springer Lecture Notes in Computer Science 242, pp. 21–47.

    Google Scholar 

  5. L. Cardelli, P. Wegner: On Understanding Types, Data Abstraction, and Polymorphism, ACM Computing Surveys 17 (1985), pp. 471–522.

    Google Scholar 

  6. P.Christensen: The Domain of CSP Processes, incomplete draft, The Technical University of Denmark, 1988.

    Google Scholar 

  7. M. Coppo, M. Dezani: A new type assignment for λ-terms, Archiv. Math. Logik 19 (1978), pp. 139–156.

    Google Scholar 

  8. T.W.Doeppner, A.Giacalone: A Formal Description of the UNIX Operating System, Proceedings of the 2nd ACM SIGACT and SIGOPS Symposium on Principles of Distributed Programming, 1983, pp. 241–253.

    Google Scholar 

  9. A.Fantechi: On combining META-IV and CCS, Proceedings of the 1984 Workshop on Formal Software Development Methods — Combining Formal Methods, Springer-Verlag.

    Google Scholar 

  10. C.A.R. Hoare: Communicating Sequential Processes, Prentice-Hall, 1985.

    Google Scholar 

  11. S.Holmström: PFL: A Functional Language for Parallel Programming, and its Implementation, Report no. 7, Programming Methodology Group, University of Gothenburgh, 1983.

    Google Scholar 

  12. J.R.Kennaway, M.R.Sleep: Expressions as processes, Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, 1982, pp. 21–28.

    Google Scholar 

  13. J.R.Kennaway, M.R.Sleep: Syntax and informal semantics of DyNe, a parallel language, Proceedings of The Analysis of Concurrent Systems (1983), Springer Lecture Notes in Computer Science 207, 1985.

    Google Scholar 

  14. D.MacQueen, G.Plotkin, R.Sethi: An ideal model for recursive polymorphic types, Proceedings of the 11th ACM Conference on Principles of Programming Languages, 1984, pp. 165–174.

    Google Scholar 

  15. R.Milner: A Calculus of Communicating Systems, Springer Lecture Notes in Computer Science 92, 1980.

    Google Scholar 

  16. F. Nielson: Strictness Analysis and Denotational Abstract Interpretation, Information and Computation 76 1 (1988) pp. 29–92.

    Google Scholar 

  17. F. Nielson, H.R. Nielson: Two-Level Semantics and Code Generation, TCS 56 (1988) pp. 59–133.

    Google Scholar 

  18. F.Nielson: Two-Level Semantics and Abstract Interpretation, TCS — Fundamental Studies (1989, to appear).

    Google Scholar 

  19. F.Nielson: A Formal Type System for Comparing Partial Evaluators, Proceedings of the 1987 IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, North-Holland, 1988.

    Google Scholar 

  20. G.D.Plotkin: A Structural Approach to Operational Semantics, Report FN-19, Aarhus University, 1981.

    Google Scholar 

  21. B.Thomsen: Higher Order CCS, Proceedings of the 1989 ACM Conference on Principles of Programming Languages, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Technical University of Denmark, DTH Building 344, DK-2800, Lyngby, Denmark

    Flemming Nielson

Authors
  1. Flemming Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eddy Odijk Martin Rem Jean-Claude Syre

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nielson, F. (1989). The typed λ-calculus with first-class processes. In: Odijk, E., Rem, M., Syre, JC. (eds) PARLE '89 Parallel Architectures and Languages Europe. PARLE 1989. Lecture Notes in Computer Science, vol 366. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51285-3_52

Download citation

  • DOI: https://doi.org/10.1007/3-540-51285-3_52

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51285-1

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation