Skip to main content

Continuation Semantics for Concurrency with Multiple Channels Communication

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9407))

Included in the following conference series:

Abstract

In this paper we investigate the formal design of concurrent languages based on the concept of continuation. We present a denotational approach of concurrent programs by using continuations for concurrency. We illustrate the approach by designing a continuation semantics for a language with nondeterministic choice, sequential and parallel composition, and a mechanism of communication and synchronization on multiple channels. For our language, we also present an operational semantics, and establish the formal relation between the denotational and operational semantics. We accomplish the semantic investigation in the mathematical framework of complete metric spaces.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We avoid to use the notion of a partially ordered multiset which is a more refined structure (see Chapt. 16 of [2]).

  2. 2.

    \(\varPi =Sched\cup \{\emptyset \}\); the set \(\varPi ={\mathcal {P}}_{fin}(Id)\) was introduced previously.

  3. 3.

    In this case the construct is used to define an ordinary set.

  4. 4.

    \((\varsigma \in )Sched={\mathcal {P}}_{nfin}(Id)\); see Sect. 3.

References

  1. America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comp. Syst. Sci. 39(3), 343–375 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  2. de Bakker, J.W., de Vink, E.P.: Control Flow Semantics. MIT Press, Cambridge (1996)

    MATH  Google Scholar 

  3. Bobrow, D.G., Wegbreit, B.: A model and stack implementation of multiple environments. Comm. ACM 16(10), 591–603 (1973)

    Article  Google Scholar 

  4. Ciobanu, G., Todoran, E.N.: Continuation semantics for concurrency. Technical report FML-09-02, Romanian Academy (2009). http://iit.iit.tuiasi.ro/TR/reports/fml0902.pdf

  5. Ciobanu, G., Todoran, E.N.: Relating two metric semantics for parallel rewriting of multisets. In: Proceedings of the SYNASC 2012, pp. 273–281. IEEE Computer Press (2012)

    Google Scholar 

  6. Ciobanu, G., Todoran, E.N.: Continuation semantics for asynchronous concurrency. Fundamenta Informaticae 131(3–4), 373–388 (2014)

    Google Scholar 

  7. Danvy, O.: On evaluation contexts, continuations and the rest of the computation. In: 4th ACM SIGPLAN Continuations Workshop, pp. 13–23 (2004)

    Google Scholar 

  8. Fournet, C., Gonthier, G.: The join calculus: a language for distributed mobile programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 268–332. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  10. Milner, R.: Fully abstract models of typed \(\lambda \)-calculi. TCS 4, 1–22 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  11. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  12. Plotkin, G.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)

    MathSciNet  MATH  Google Scholar 

  13. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1997)

    Google Scholar 

  14. Stratchey, C., Wadsworth, C.: Continuations: a mathematical semantics for handling full jumps. Higher-Order Symbolic Comput. 13, 135–152 (2000)

    Article  MATH  Google Scholar 

  15. Todoran, E.N.: Metric semantics for synchronous and asynchronous communication: a continuation-based approach. ENTCS 28, 119–146 (2000)

    Google Scholar 

Download references

Acknowledgements

This research was supported by the Romanian National Authority for Scientific Research, project number PN-II-ID-PCE-2011-3-0919.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Eneia Nicolae Todoran .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ciobanu, G., Todoran, E.N. (2015). Continuation Semantics for Concurrency with Multiple Channels Communication. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25423-4_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25422-7

  • Online ISBN: 978-3-319-25423-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics