Skip to main content
SpringerLink
Log in

Topological models for higher order control flow

  • Conference paper
  • First Online:
Mathematical Foundations of Programming Semantics (MFPS 1993)

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

Abstract

Semantic models are presented for two simple imperative languages with higher order constructs. In the first language the interesting notion is that of second order assignment x:=s, for x a procedure variable and s a statement. The second language extends this idea by a form of higher order communication, with statements c! s and c? x, for c a channel. We develop operational and denotational models for both languages, and study their relationships. Both in the definitions and the comparisons of the semantic models, convenient use is made of some tools from (metric) topology. The operational models are based on (SOS-style) transition systems; the denotational definitions use domains specified as solutions of domain equations in a category of 1-bounded complete ultrametric spaces. In establishing the connection between the two kinds of models, fruitful use is made of Rutten's processes as terms technique. Another new tool consists in the use of metric transition systems, with a metric defined on the configurations of the system. In addition to higher order programming notions, we use higher order definitional techniques, e.g., in defining the semantic mappings as fixed points of (contractive) higher order operators. By Banach's theorem, such fixed points are unique, yielding another important proof principle for our paper.

This work was partially supported by the Netherlands Nationale Faciliteit Informatica programme, project Research and Education in Concurrent Systems (REX).

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. America, J.W. de Bakker, J.N. Kok, and J.J.M.M. Rutten. Denotational Semantics of a Parallel Object-Oriented Language. Information and Computation, 83(2): 152–205, November 1989.

    Google Scholar 

  2. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. In Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 31–46, San Francisco, January 1990.

    Google Scholar 

  3. E. Astesiano, A. Giovini, and G. Reggio. Observational Structures and their Logics. Theoretical Computer Science, 96(1):249–283, April 1992.

    Google Scholar 

  4. E. Astesiano and G. Reggio. SMoLCS-driven Concurrent Calculi. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 249 of Lecture Notes in Computer Science, pages 169–201, Pisa, March 1987. Springer-Verlag.

    Google Scholar 

  5. P. America and J.J.M.M. Rutten. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. Journal of Computer and System Sciences, 39(3):343–375, December 1989.

    Google Scholar 

  6. S. Banach. Sur les Opérations dans les Ensembles Abstraits et leurs Applications aux Equations Intégrales. Fundamenta Mathematicae, 3:133–181, 1922.

    Google Scholar 

  7. H.P. Barendregt. Lambda Calculi with Types. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, Background: Computational Structures, chapter 2, pages 117–309. Clarendon Press, Oxford, 1992.

    Google Scholar 

  8. G. Berry and G. Boudol. The Chemical Abstract Machine. Theoretical Computer Science, 96(1):217–248, April 1992.

    Google Scholar 

  9. J.W. de Bakker and J.-J.Ch. Meyer. Metric Semantics for Concurrency. BIT, 28:504–529, 1988.

    Google Scholar 

  10. G. Boudol. Towards a Lambda-Calculus for Concurrent and Communicating Systems. In J. Diaz and F. Orejas, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 351 of Lecture Notes in Computer Science, pages 149–162, Barcelona, March 1989. Springer-Verlag.

    Google Scholar 

  11. J.W. de Bakker and J.J.M.M. Rutten, editors. Ten Years of Concurrency Semantics, selected papers of the Amsterdam Concurrency Group. World Scientific, Singapore, September 1992.

    Google Scholar 

  12. F. van Breugel. Three Metric Domains of Processes for Bisimulation. This volume.

    Google Scholar 

  13. F. van Breugel. Topological Models in Comparative Semantics. PhD thesis, Vrije Universiteit, Amsterdam, 1994. In preparation.

    Google Scholar 

  14. J.W. de Bakker and J.I. Zucker. Processes and the Denotational Semantics of Concurrency. Information and Control, 54(1/2):70–120, July/August 1982.

    Google Scholar 

  15. P.-L. Curien. The λρ-calculus: An Abstract Framework for Environment Machines. Report, LIENS, Paris, October 1988.

    Google Scholar 

  16. C.A.R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice/Hall International, London, 1985.

    Google Scholar 

  17. R. Jagadeesan and P. Panangaden. A Domain-theoretic Model for a Higherorder Process Calculus. In M.S. Paterson, editor, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 181–194, Coventry, July 1990. Springer-Verlag.

    Google Scholar 

  18. J.N. Kok and J.J.M.M. Rutten. Contractions in Comparing Concurrency Semantics. Theoretical Computer Science, 76(2/3):179–222, 1990.

    Google Scholar 

  19. K. Kuratowski. Sur une Méthode de Métrisation Complète des Certains Espaces d'Ensembles Compacts. Fundamenta Mathematicae, 43:114–138, 1956.

    Google Scholar 

  20. J.-J. Lévy, B. Thomsen, L. Leth, and A. Giacalone. CONcurrency and Functions: Evaluation and Reduction. Bulletin of the European Association for Theoretical Computer Science, 48:88–106, October 1992.

    Google Scholar 

  21. E. Michael. Topologies on Spaces of Subsets. Transactions of the American Mathematical Society, 71:152–182, 1951.

    Google Scholar 

  22. R. Milner. Functions as Processes. Mathematical Structures in Computer Science, 2(2):119–141, June 1992.

    Google Scholar 

  23. R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, I and II. Information and Computation, 1(100):1–40 and 41–77, September 1992.

    Google Scholar 

  24. R. Milner and D. Sangiorgi. Barbed Bisimulation. In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science, pages 685–695, Vienna, July 1992. Springer-Verlag.

    Google Scholar 

  25. G.D. Plotkin. A Structural Approach to Operational Semantics. Report DAIMI FN-19, Aarhus University, Aarhus, September 1981.

    Google Scholar 

  26. J.J.M.M. Rutten and D. Turi. On the Foundations of Final Semantics: non-standard sets, metric spaces, partial orders. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop on Semantics: Foundations and Applications, volume 666 of Lecture Notes in Computer Science, pages 477–530, Beekbergen, June 1992. Springer-Verlag.

    Google Scholar 

  27. J.J.M.M. Rutten. Processes as Terms: Non-Well-Founded Models for Bisimulation. Mathematical Structures in Computer Science, 2(3):257–275, September 1992.

    Google Scholar 

  28. D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburg, Edinburg, 1992.

    Google Scholar 

  29. D. Sangiorgi. An Investigation into Functions as Processes. This volume.

    Google Scholar 

  30. B. Thomsen. A Calculus of Higher Order Communicating Systems. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, pages 143–154, Austin, January 1989.

    Google Scholar 

  31. B. Thomsen. Calculi for Higher Order Communicating Systems. PhD thesis, Imperial College, London, September 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Technology, CWI, Kruislaan 413, 1098, SJ Amsterdam

    J. W. de Bakker & F. van Breugel

  2. Department of Mathematics and Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081, HV Amsterdam

    J. W. de Bakker & F. van Breugel

Authors
  1. J. W. de Bakker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. F. van Breugel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stephen Brookes Michael Main Austin Melton Michael Mislove David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Bakker, J.W., van Breugel, F. (1994). Topological models for higher order control flow. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-58027-1_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58027-0

  • Online ISBN: 978-3-540-48419-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation